Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

40

CADE
2008
Springer

favoriteEmaildiscussreport

131views Logical Reasoning» more CADE 2008»

Linear Quantifier Elimination

14 years 11 months ago

Linear Quantifier Elimination

Download www4.informatik.tu-muenchen.de

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).

Tobias Nipkow

Real-time Traffic

Automated Reasoning | CADE 2008 | Quantifier Elimination Procedures | Theorem Prover Isabelle/hol |

claim paper

Related Content

» Verifying Mixed RealInteger Quantifier Elimination

» QuantifierElimination for the FirstOrder Theory of Boolean Algebras with Linear Cardinalit...

» A Quantifier Elimination Algorithm for Linear Real Arithmetic

» Weak Integer Quantifier Elimination Beyond the Linear Case

» New Domains for Applied Quantifier Elimination

» Interpolating QuantifierFree Presburger Arithmetic

» Parametric Linear Arithmetic over Ordered Fields in IsabelleHOL

» Generic Hermitian Quantifier Elimination

» Proof Synthesis and Reflection for Linear Arithmetic

Post Info
More Details (n/a)

Added	03 Dec 2009
Updated	03 Dec 2009
Type	Conference
Year	2008
Where	CADE
Authors	Tobias Nipkow

Comments (0)