TY - GEN
T1 - Linear quantifier elimination
AU - Nipkow, Tobias
PY - 2008
Y1 - 2008
N2 - 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).
AB - 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).
UR - http://www.scopus.com/inward/record.url?scp=53049110148&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-71070-7_3
DO - 10.1007/978-3-540-71070-7_3
M3 - Conference contribution
AN - SCOPUS:53049110148
SN - 3540710698
SN - 9783540710691
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 18
EP - 33
BT - Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings
T2 - 4th International Joint Conference on Automated Reasoning, IJCAR 2008
Y2 - 12 August 2008 through 15 August 2008
ER -