Verifying and reflecting quantifier elimination for presburger arithmetic

Amine Chaieb, Tobias Nipkow

Research output: Contribution to journalConference articlepeer-review

15 Scopus citations

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.

Fingerprint

Dive into the research topics of 'Verifying and reflecting quantifier elimination for presburger arithmetic'. Together they form a unique fingerprint.

Cite this