2014 | OriginalPaper | Buchkapitel
Real Quantifier Elimination in the RegularChains Library
verfasst von : Changbo Chen, Marc Moreno Maza
Erschienen in: Mathematical Software – ICMS 2014
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Quantifier elimination (QE) over real closed fields has found numerous applications. Cylindrical algebraic decomposition (CAD) is one of the main tools for handling quantifier elimination of nonlinear input formulas. Despite of its worst case doubly exponential complexity, CAD-based quantifier elimination remains interesting for handling general quantified formulas and producing simple quantifier-free formulas.
In this paper, we report on the implementation of a QE procedure, called
QuantifierElimination
, based on the CAD implementations in the
RegularChains
library. This command supports both standard quantifier-free formula and extended Tarski formula in the output. The use of the QE procedure is illustrated by solving examples from different applications.