Relatively complete and efficient partial quantifier elimination

DOI10.1007/978-3-031-99984-0_26MaRDI QIDQ6869933zbMATH OpenFDO

Authors Estifanos Getachew, Arie Gurfinkel, Richard Trefler

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_26

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A mathematical introduction to logic.
• An algorithm for reasoning about equality
• An efficient quantifier elimination procedure for Presburger arithmetic
• Automated Deduction – CADE-20
• Automatic recognition of tractability in inference relations
• Decision procedures. An algorithmic point of view
• Fast approximations of quantifier elimination
• scientific article; zbMATH DE number 53151 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• MCMT: a model checker modulo theories
• Polynomial-time computation via local inference relations
• Real quantifier elimination is doubly exponential
• Reasoning About Recursively Defined Data Structures
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee

This page was built for publication: Relatively complete and efficient partial quantifier elimination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869933)