KMS Chongqing Institute of Green and Intelligent Technology, CAS
| Real quantifier elimination in the RegularChains library | |
| Chen, Changbo1; Moreno Maza, Marc2 | |
| 2014 | |
| 摘要 | 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. © 2014 Springer-Verlag. |
| 语种 | 英语 |
| DOI | 10.1007/978-3-662-44199-2_44 |
| 会议(录)名称 | 4th International Congress on Mathematical Software, ICMS 2014
 |
| 页码 | 283-290 |
| 收录类别 | EI |
| 会议地点 | Seoul, Korea, Republic of |
| 会议日期 | August 5, 2014 - August 9, 2014 |
