×

Better answers to real questions. (English) Zbl 1346.68290

Summary: We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination for the quadratic case via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.

MSC:

68W30 Symbolic computation and algebraic computation
03C10 Quantifier elimination, model completeness, and related topics

Software:

REDLOG
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Akritas, A. G., Linear and quadratic complexity bounds on the values of the positive roots of polynomials, J. Univers. Comput. Sci., 15, 523-537 (2009) · Zbl 1216.65053
[2] Boulier, F.; Lefranc, M.; Lemaire, F.; Morant, P. E.; Ürgüplü, A., On proving the absence of oscillations in models of genetic circuits, (Anai, H.; Horimoto, K.; Kutsia, T., Proceedings of Algebraic Biology. Proceedings of Algebraic Biology, Lect. Notes Comput. Sci., vol. 4545 (2007)), 66-80 · Zbl 1127.92306
[3] Burhenne, K. D., Implementierung eines Algorithmus zur Quantorenelimination fur lineare reelle Probleme (1990), Universität Passau: Universität Passau Germany, Diplomarbeit
[4] Collard, J. F., Reasoning about Program Transformations (2003), Springer
[5] Dolzmann, A.; Gloor, O.; Sturm, T., Approaches to parallel quantifier elimination, (Gloor, O., Proceedings of the ISSAC 98 (1998), ACM Press), 88-95 · Zbl 0918.68054
[6] Dolzmann, A.; Sturm, T., Redlog: computer algebra meets computer logic, ACM SIGSAM Bull., 31, 2-9 (1997)
[7] Dolzmann, A.; Sturm, T., Simplification of quantifier-free formulae over ordered fields, J. Symb. Comput., 24, 209-231 (1997) · Zbl 0882.03030
[8] Dolzmann, A.; Sturm, T., Redlog user manual, 2nd edition (1999), FMI, Universität Passau: FMI, Universität Passau Germany, Technical Report MIP-9905
[9] Dolzmann, A.; Sturm, T.; Weispfenning, V., A new approach for automatic theorem proving in real geometry, J. Autom. Reason., 21, 357-380 (1998) · Zbl 0914.03013
[10] Dolzmann, A.; Sturm, T.; Weispfenning, V., Real quantifier elimination in practice, (Matzat, B. H.; Greuel, G. M.; Hiss, G., Algorithmic Algebra and Number Theory (1999), Springer), 221-247 · Zbl 0934.68130
[11] El Kahoui, M.; Weber, A., Deciding Hopf bifurcations by quantifier elimination in a software component architecture, J. Symb. Comput., 30, 161-179 (2000) · Zbl 0965.65137
[12] Errami, H.; Eiswirth, M.; Grigoriev, D.; Seiler, W. M.; Sturm, T.; Weber, A., Efficient methods to compute Hopf bifurcations in chemical reaction networks using reaction coordinates, (Proceedings of the CASC 2013. Proceedings of the CASC 2013, Lect. Notes Comput. Sci., vol. 8136 (2013)), 88-99 · Zbl 1412.34132
[13] Errami, H.; Eiswirth, M.; Grigoriev, D.; Seiler, W. M.; Sturm, T.; Weber, A., Detection of Hopf bifurcations in chemical reaction networks using convex coordinates, J. Comput. Phys., 291, 279-302 (2015) · Zbl 1349.92168
[14] Errami, H.; Sturm, T.; Weber, A., Algorithmic aspects of Muldowney’s extension of the Bendixson-Dulac criterion for polynomial vector fields, (Vassiliev, N. N., Polynomial Computer Algebra (2011), The Euler International Mathematical Institute: The Euler International Mathematical Institute St. Petersburg, Russia), 25-28
[15] Gatermann, K.; Eiswirth, M.; Sensse, A., Toric ideals and graph theory to analyze Hopf bifurcations in mass action systems, J. Symb. Comput., 40, 1361-1382 (2005) · Zbl 1120.13033
[16] Korovin, K.; Tsiskaridze, N.; Voronkov, A., Conflict resolution, (Gent, I. P., Principles and Practice of Constraint Programming - CP 2009. Principles and Practice of Constraint Programming - CP 2009, Lect. Notes Comput. Sci., vol. 5732 (2009)), 509-523 · Zbl 1336.68236
[17] Lasaruk, A.; Sturm, T., Weak quantifier elimination for the full linear theory of the integers. A uniform generalization of Presburger arithmetic, Appl. Algebra Eng. Commun. Comput., 18, 545-574 (2007) · Zbl 1154.68112
[18] Loos, R.; Weispfenning, V., Applying linear quantifier elimination, Comput. J., 36, 450-462 (1993) · Zbl 0787.03021
[19] Nelson, G.; Oppen, D. C., Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst., 1, 245-257 (1979) · Zbl 0452.68013
[20] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), J. ACM, 53, 937-977 (2006) · Zbl 1326.68164
[21] Seidl, A. M.; Sturm, T., Boolean quantification in a first-order context, (Ganzha, V. G.; Mayr, E. W.; Vorozhtsov, E. V., Computer Algebra in Scientific Computing. Proceedings of the CASC 2003 (2003), Institut für Informatik, Technische Universität München: Institut für Informatik, Technische Universität München München, Germany), 329-345
[22] Sturm, T., Real quantifier elimination in geometry (1999), Universität Passau: Universität Passau Germany, Doctoral dissertation
[23] Sturm, T., Reasoning over networks by symbolic methods, Appl. Algebra Eng. Commun. Comput., 10, 79-96 (1999) · Zbl 0931.68142
[24] Sturm, T., An algebraic approach to offsetting and blending of solids, (Ganzha, V. G.; Mayr, E. W.; Vorozhtsov, E. V., Computer Algebra in Scientific Computing. Proceedings of the CASC 2000 (2000), Springer: Springer Berlin), 367-382 · Zbl 0976.68167
[25] Sturm, T., Linear problems in valued fields, J. Symb. Comput., 30, 207-219 (2000) · Zbl 0982.03018
[26] Sturm, T.; Tiwari, A., Verification and synthesis using real quantifier elimination, (Proceedings of the ISSAC 2011 (2011), ACM Press), 329-336 · Zbl 1323.68385
[27] Sturm, T.; Weber, A., Investigating generic methods to solve Hopf bifurcation problems in algebraic biology, (Horimoto, K., Proceedings of Algebraic Biology 2008. Proceedings of Algebraic Biology 2008, Lect. Notes Comput. Sci., vol. 5147 (2008)), 200-215 · Zbl 1171.92301
[28] Sturm, T.; Weber, A.; Abdel-Rahman, E. O.; El Kahoui, M., Investigating algebraic and logical algorithms to solve Hopf bifurcation problems in algebraic biology, Math. Comput. Sci., 2, 493-515 (2009) · Zbl 1205.37062
[29] Sturm, T.; Weispfenning, V., Computational geometry problems in REDLOG, (Wang, D., Automated Deduction in Geometry. Automated Deduction in Geometry, LNAI, vol. 1360 (1997)), 58-86 · Zbl 0904.65151
[30] Sturm, T.; Weispfenning, V., Rounding and blending of solids by a real elimination method, (Sydow, A., Proceedings of the IMACS 97, vol. 2 (1997), Wissenschaft & Technik Verlag: Wissenschaft & Technik Verlag Berlin), 727-732
[31] Sturm, T.; Weispfenning, V., Quantifier elimination in term algebras. The case of finite languages, (Ganzha, V. G.; Mayr, E. W.; Vorozhtsov, E. V., Computer Algebra in Scientific Computing. Proceedings of the CASC 2002 (2002), Institut für Informatik, Technische Universität München: Institut für Informatik, Technische Universität München Garching, Germany), 285-300
[32] Sturm, T.; Zengler, C., Parametric quantified SAT solving, (Watt, S. M., Proceedings of the ISSAC 2010 (2010), ACM Press), 77-84 · Zbl 1321.68322
[33] Weber, A.; Sturm, T.; Abdel-Rahman, E. O., Algorithmic global criteria for excluding oscillations, Bull. Math. Biol., 73, 899-916 (2011) · Zbl 1214.92002
[34] Weispfenning, V., The complexity of linear problems in fields, J. Symb. Comput., 5, 3-27 (1988) · Zbl 0646.03005
[35] Weispfenning, V., Parametric linear and quadratic optimization by elimination (1994), Universität Passau: Universität Passau Germany, Technical Report MIP-9404
[36] Weispfenning, V., Quantifier elimination for real algebra—the cubic case, (Proceedings of the ISSAC 1994 (1994), ACM Press), 258-263 · Zbl 0919.03030
[37] Weispfenning, V., Quantifier elimination for real algebra—the quadratic case and beyond, Appl. Algebra Eng. Commun. Comput., 8, 85-101 (1997) · Zbl 0867.03003
[38] Weispfenning, V., Simulation and optimization by quantifier elimination, J. Symb. Comput., 24, 189-208 (1997) · Zbl 0883.68075
[39] Weispfenning, V., Semilinear motion planning in REDLOG, Appl. Algebra Eng. Commun. Comput., 12, 455-475 (2001) · Zbl 1003.65015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.