Verifying and reflecting quantifier elimination for Presburger arithmetic

Amine Chaieb Tobias Nipkow,

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}