Linear Quantifier Elimination

Abstract. This paper presents verified quantifier elimination procedures for dense linear orders (DLO), for real and for integer linear arithmetic. The DLO procedures are new. All procedures are defined and verified in the theorem prover Isabelle/HOL, are executable and can be applied to HOL formulae themselves (by reflection).

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Tobias Nipkow
• Keywords: Automated Reasoning, CADE 2008, Quantifier Elimination Procedures, Theorem Prover Isabelle/hol