Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic.

Authors :: Sutcliffe, Geoff
Voronkov, Andrei
Chaieb, Amine
Nipkow, Tobias
Source :: Logic for Programming, Artificial Intelligence & Reasoning (9783540305538); 2005, p367-380, 14p
Publication Year :: 2005
Abstract: We present an implementation and verification in higher-order logic of Cooper's quantifier elimination for Presburger arithmetic. Reflection, i.e. the direct execution in ML, yields a speed-up of a factor of 200 over an LCF-style implementation and performs as well as a decision procedure hand-coded in ML. [ABSTRACT FROM AUTHOR]

Language :: English
ISBNs :: 9783540305538
Database :: Supplemental Index
Journal :: Logic for Programming, Artificial Intelligence & Reasoning (9783540305538)
Publication Type :: Book
Accession number :: 32905055
Full Text :: https://doi.org/10.1007/11591191_26