Proving theorems with quantifier elimination techniques
Quantifier elimination techniques constitute important tools for showing decidability results for various mathematical theories. But the decision procedures for satisfiability / provability that are based on quantifier elimination are often prohibitively expensive. Nonetheless, a practical use of quantifier elimination in decision procedures emerged in the field of SMT-solving to decide the satisfiability of (rather surprisingly) quantifier-free formulae. We describe the approach, illustrating it with the case of linear arithmetic and reviewing the key ingredients that make the approach of practical use and that contrast with standard quantifier elimination. We highlight the proof construction aspect and its duality with the model construction one (in terms of which satisfiability techniques are often phrased). We will then describe the current research leads for generalising this approach to quantified formulae, in connection to contributions by Bjørner and Janota that approach the satisfiability of quantified formulae in terms of a game.
Back to the main page