Symbolelimination und Quantorenelimination und Anwendungen

Symbol elimination in general and quantifier elimination in particular are important in different areas nowadays: In verification, symbol elimination is used e.g. in CEGAR procedures (Counterexample-Guided Abstraction Refinement) or in the automatic generation of invariants. In the verification of parametric systems it is often important to generate constraints on parameters to ensure the safety of such systems. In databases, symbol limination is used to model ``forgetting''. In mathematics, such methods are used in particular for the automatic proof of theorems in analytic geometry.

The goal of this project is to investigate methods for symbol elimination and quantifier elimination in various theories. Ultimately, we would like to develop methods for symbol elimination in complex theories that exploit the modular structure of the theories and allow specialized methods for symbol elimination and/or quantifier elimination to be used in a modular fashion for individual theories, and to analyze applications of such methods in verification, in the analysis of databases, and in geometry.