Real quantifier elimination in the RegularChains library
文献类型：会议论文
| 作者 | Chen, Changbo1; Moreno Maza, Marc2 |
| 出版日期 | 2014 |
| 会议日期 | August 5, 2014 - August 9, 2014 |
| 会议地点 | Seoul, Korea, Republic of |
| DOI | 10.1007/978-3-662-44199-2_44 |
| 页码 | 283-290 |
| 英文摘要 | 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. |
| 会议录 | 4th International Congress on Mathematical Software, ICMS 2014
 |
| 语种 | 英语 |
| 电子版国际标准刊号 | 16113349 |
| ISSN号 | 03029743 |
| 源URL | [http://119.78.100.138/handle/2HOD01W0/4801]  |
| 专题 | 自动推理与认知研究中心 |
| 作者单位 | 1.Chongqing Key Laboratory of Automated Reasoning and Cognition, Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences, China; 2.ORCCA, University of Western Ontario, Canada |
| 推荐引用方式 GB/T 7714 | Chen, Changbo,Moreno Maza, Marc. Real quantifier elimination in the RegularChains library[C]. 见:. Seoul, Korea, Republic of. August 5, 2014 - August 9, 2014. |
入库方式： OAI收割
来源：重庆绿色智能技术研究院
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。