Verifying and reflecting quantifier elimination for Presburger arithmetic
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.
pdf
SpringerLink
BibTeX:
@inproceedings{ChaiebN-LPAR05,
author={Amine Chaieb and Tobias Nipkow},
title={Verifying and reflecting quantifier elimination for Presburger arithmetic},
booktitle={Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2005)},
editor={G. Sutcliffe and A. Voronkov},
publisher=Springer,series=LNCS,volume=3835,pages={367-380},year=2005}