A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications

被引：15
作者：
Sturm T. [1 ,2 ]
机构：
[1] University of Lorraine, CNRS, Inria, and LORIA, Nancy
[2] Max Planck Institute for Informatics and Saarland University, Saarbrücken Informatics Campus, Saarbrücken
来源：
Mathematics in Computer Science | 2017年 / 11卷 / 3-4期
关键词：
Reaction systems; Real geometry; Real quantifier elimination and decision; Satisfiability; Stability analysis; Subtropical methods; Verification; Virtual substitution;
D O I：
10.1007/s11786-017-0319-z
中图分类号：
学科分类号：
摘要：
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. © 2017, The Author(s).
引用
收藏
页码：483 / 502
页数：19
相关论文
共 75 条
[1]  
Arnon D.S., Algorithms for the geometry of semi-algebraic sets, Technical Report, 436, (1981)
[2]  
Basu S., Pollack R., Roy M.-F., On the combinatorial and algebraic complexity of quantifier elimination, J. ACM, 43, 6, pp. 1002-1045, (1996)
[3]  
Boulier F., Lefranc M., Lemaire F., Morant P.-E., Urguplu A., On proving the absence of oscillations in models of genetic circuits, Proceedings of the AB 2007, volume 4545 of LNCS, pp. 66–80. Springer, (2007)
[4]  
Boulier F., Lefranc M., Lemaire F., Morant P.-E., Applying a rigorous quasi-steady state approximation method for proving the absence of oscillations in models of genetic circuits, Proceedings of the AB 2008, volume 5147 of LNCS, pp. 56–64. Springer, (2008)
[5]  
Brown C.W., Gross C., Efficient preprocessing methods for quantifier elimination, Proceedings of the CASC 2006, volume 4194 of LNCS, pp. 89–100. Springer, (2006)
[6]  
Brown C.W., QEPCAD B: a program for computing with semi-algebraic sets using CADs, ACM SIGSAM Bull., 37, 4, pp. 97-108, (2003)
[7]  
Brown C.W., Kosta M., Constructing a single cell in cylindrical algebraic decomposition, J. Symb. Comput., 70, pp. 14-48, (2014)
[8]  
Buchberger B., Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Doctoral dissertation, Mathematical Institute, University of Innsbruck, (1965)
[9]  
Chou S.-C., Mechanical Geometry Theorem Proving. Mathematics and Its Applications, (1988)
[10]  
Clarke B.L., Stability of complex reaction networks, Advances in Chemical Physics, (1980)
12345678