Verifying Mixed Real-Integer Quantifier Elimination

Abstract. We present a formally verified quantifier elimination procedure for the first order theory over linear mixed real-integer arithmetics in higher-order logic based on a work by Weispfenning. To this end we provide two verified quantifier elimination procedures: for Presburger arithmitics and for linear real arithmetics.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Amine Chaieb
• Keywords: Automated Reasoning, CADE 2006, Quantifier Elimination Procedure, Quantifier Elimination Procedures, Verified Quantifier Elimination