Verifying and reflecting quantifier elimination for presburger arithmetic

Amine Chaieb, Tobias Nipkow

Publikation: Beitrag in FachzeitschriftKonferenzartikelBegutachtung

15 Zitate (Scopus)

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.

OriginalspracheEnglisch
Seiten (von - bis)367-380
Seitenumfang14
FachzeitschriftLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Jahrgang3835 LNAI
DOIs
PublikationsstatusVeröffentlicht - 2005
Veranstaltung12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005 - Montego Bay, Jamaika
Dauer: 2 Dez. 20056 Dez. 2005

Fingerprint

Untersuchen Sie die Forschungsthemen von „Verifying and reflecting quantifier elimination for presburger arithmetic“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren