A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications
A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications
复制标题
DOI：
10.1007/s11786-017-0319-z
复制
发表时间：
2017-12-01
影响因子：
0.8
通讯作者：
Sturm, Thomas
中科院分区：
文献类型：
--
作者：
Sturm, Thomas
一阶理论的有效量词消除过程为基于逻辑规范一般性地解决各种问题提供了强大的工具。与一般的一阶证明者相比，量词消除过程基于一组固定的可接受的逻辑符号，具有隐式固定的语义。这允许使用符号计算的子算法。我们将重点关注实数的量词消除及其应用，并给出几何、验证和生命科学的示例。除了量词消除之外，我们还将讨论实数存在片段的亚热带程序的最新结果。这种不完全决策程序已成功应用于化学和生命科学中的反应系统分析。
Effective quantifier elimination procedures for first-order theories provide a powerful tool for generically solving a wide range of problems based on logical specifications. In contrast to general first-order provers, quantifier elimination procedures are based on a fixed set of admissible logical symbols with an implicitly fixed semantics. This admits the use of sub-algorithms from symbolic computation. We are going to focus on quantifier elimination for the reals and its applications giving examples from geometry, verification, and the life sciences. Beyond quantifier elimination we are going to discuss recent results with a subtropical procedure for an existential fragment of the reals. This incomplete decision procedure has been successfully applied to the analysis of reaction systems in chemistry and in the life sciences.