Verifying and reflecting quantifier elimination for presburger arithmetic

Amine Chaieb; Tobias Nipkow

doi:10.1007/11591191_26

Verifying and reflecting quantifier elimination for presburger arithmetic

Amine Chaieb, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Contribution to journal › Conference article › peer-review

16 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.

Original language	English
Pages (from-to)	367-380
Number of pages	14
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3835 LNAI
DOIs	https://doi.org/10.1007/11591191_26
State	Published - 2005
Event	12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005 - Montego Bay, Jamaica Duration: 2 Dec 2005 → 6 Dec 2005

Access to Document

10.1007/11591191_26

Cite this

@article{45083cb0662845b1b65ee34190efd2fd,

title = "Verifying and reflecting quantifier elimination for presburger arithmetic",

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.",

author = "Amine Chaieb and Tobias Nipkow",

year = "2005",

doi = "10.1007/11591191_26",

language = "English",

volume = "3835 LNAI",

pages = "367--380",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

note = "12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005 ; Conference date: 02-12-2005 Through 06-12-2005",

}

TY - JOUR

T1 - Verifying and reflecting quantifier elimination for presburger arithmetic

AU - Chaieb, Amine

AU - Nipkow, Tobias

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33745462323&partnerID=8YFLogxK

U2 - 10.1007/11591191_26

DO - 10.1007/11591191_26

M3 - Conference article

AN - SCOPUS:33745462323

SN - 0302-9743

VL - 3835 LNAI

SP - 367

EP - 380

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005

Y2 - 2 December 2005 through 6 December 2005

ER -

Verifying and reflecting quantifier elimination for presburger arithmetic

Abstract

Access to Document

Other files and links

Fingerprint

Cite this