Sciweavers

CADE
2006
Springer
15 years 23 days ago
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 wor...
Amine Chaieb
CADE
2008
Springer
15 years 23 days ago
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 ...
Tobias Nipkow