Skip to main content
Conference Proceedings

Verifying mixed real-integer quantifier elimination

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2006) 4130 LNAI 528-540
DOI: 10.1007/11814771_43
9Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We present a formally verified quantifier elimination procedure for the first order theory over linear mixed real-integer arithmetics in higher-order logic based on a work by Weispfenning. To this end we provide two verified quantifier elimination procedures: for Presburger arithmitics and for linear real arithmetics. © Springer-Verlag Berlin Heidelberg 2006.

Cite

CITATION STYLE

APA

Chaieb, A. (2006). Verifying mixed real-integer quantifier elimination. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4130 LNAI, pp. 528–540). Springer Verlag. https://doi.org/10.1007/11814771_43

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free