Advertisement
Published in:
2014 | OriginalPaper | Chapter
Real Quantifier Elimination in the RegularChains Library
Authors : Changbo Chen, Marc Moreno Maza
Published in: Mathematical Software – ICMS 2014
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.