On the generation of Positivstellensatz witnesses in degenerate cases. (English) Zbl 1342.68296
Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 249-264 (2011).
Summary: One can reduce the problem of proving that a polynomial is nonnegative, or more generally of proving that a system of polynomial inequalities has no solutions, to finding polynomials that are sums of squares of polynomials and satisfy some linear equality (Positivstellensatz). This produces a witness for the desired property, from which it is reasonably easy to obtain a formal proof of the property suitable for a proof assistant such as Coq.
The problem of finding a witness reduces to a feasibility problem in semidefinite programming, for which there exist numerical solvers. Unfortunately, this problem is in general not strictly feasible, meaning the solution can be a convex set with empty interior, in which case the numerical optimization method fails. Previously published methods thus assumed strict feasibility; we propose a workaround for this difficulty.
We implemented our method and illustrate its use with examples, including extractions of proofs to Coq.
For the entire collection see [Zbl 1219.68024].
The problem of finding a witness reduces to a feasibility problem in semidefinite programming, for which there exist numerical solvers. Unfortunately, this problem is in general not strictly feasible, meaning the solution can be a convex set with empty interior, in which case the numerical optimization method fails. Previously published methods thus assumed strict feasibility; we propose a workaround for this difficulty.
We implemented our method and illustrate its use with examples, including extractions of proofs to Coq.
For the entire collection see [Zbl 1219.68024].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03C10 | Quantifier elimination, model completeness, and related topics |
| 12D15 | Fields related with sums of squares (formally real fields, Pythagorean fields, etc.) |
References:
| [1] | Adams, J., Saunders, B.D., Wan, Z.: Signature of symmetric rational matrices and the unitary dual of Lie groups. In: ISSAC 2005, pp. 13–20. ACM, New York (2005) · Zbl 1360.65116 |
| [2] | Basu, S., Pollack, R., Roy, M.-F.: On the combinatorial and algebraic complexity of quantifier elimination. Journal of the ACM (JACM) 43(6), 1002–1045 (1996) · Zbl 0885.68070 · doi:10.1145/235809.235813 |
| [3] | Benson, S.J., Ye, Y.: DSDP5 user guide – software for semidefinite programming. technical memorandum 277. Argonne National Laboratory (2005) |
| [4] | Benson, S.J., Ye, Y.: Algorithm 875: DSDP5–software for semidefinite programming. ACM Transactions on Mathematical Software 34(3), 16:1–16:20 (2008) · Zbl 1291.65173 |
| [5] | Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2007) · Zbl 1178.03020 · doi:10.1007/978-3-540-74464-1_4 |
| [6] | Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004), http://www.stanford.edu/ boyd/cvxbook/ · Zbl 1058.90049 · doi:10.1017/CBO9780511804441 |
| [7] | Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975) · doi:10.1007/3-540-07407-4_17 |
| [8] | Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition – twenty years of progress. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 8–23 (1998) · Zbl 0900.03053 · doi:10.1007/978-3-7091-9459-1_2 |
| [9] | Coste, M., Lombardi, H., Roy, M.F.: Dynamical method in algebra: effective Nullstellensätze. Annals of Pure and Applied Logic 111(3), 203–256 (2001); Proceedings of the International Conference ”Analyse & Logique” Mons, Belgium, August 25-29 (1997) · Zbl 0992.03076 · doi:10.1016/S0168-0072(01)00026-4 |
| [10] | Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Tech. Rep. SRI-CSL-06-01, SRI International (May 2006) |
| [11] | Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102–118. Springer, Heidelberg (2007) · Zbl 1144.68357 · doi:10.1007/978-3-540-74591-4_9 |
| [12] | INRIA: The Coq Proof Assistant Reference Manual, 8.1 edn. (2006) |
| [13] | Kaltofen, E., Li, B., Yang, Z., Zhi, L.: Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars. In: ISSAC (International Symposium on Symbolic and Algebraic Computation), pp. 155–163. ACM, New York (2008) |
| [14] | Kaltofen, E., Li, B., Yang, Z., Zhi, L.: Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients (2009), accepted at J. Symbolic Computation · Zbl 1229.90115 |
| [15] | de Klerk, E., Pasechnik, D.V.: Products of positive forms, linear matrix inequalities, and Hilbert 17th problem for ternary forms. European Journal of Operational Research, 39–45 (2004) · Zbl 1106.90058 · doi:10.1016/j.ejor.2003.08.014 |
| [16] | Krivine, J.L.: Anneaux préordonnés. J. Analyse Math. 12, 307–326 (1964), http://hal.archives-ouvertes.fr/hal-00165658/en/ · Zbl 0134.03902 · doi:10.1007/BF02807438 |
| [17] | Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008) · Zbl 1149.68071 |
| [18] | Lombardi, H.: Théorème des zéros réels effectif et variantes. Tech. rep., Université de Franche-Comté, Besan con, France (1990), http://hlombardi.free.fr/publis/ThZerMaj.pdf |
| [19] | Lombardi, H.: Une borne sur les degrés pour le théorème des zéros réel effectif. In: Coste, M., Mahé, L., Roy, M.F. (eds.) Real Algebraic Geometry: Proceedings of the Conference held in Rennes, France. Lecture Notes in Mathematics, vol. 1524, Springer, Heidelberg (1992) · doi:10.1007/BFb0084631 |
| [20] | Mahboubi, A.: Implementing the CAD algorithm inside the Coq system. Mathematical Structures in Computer Sciences 17(1) (2007) · Zbl 1121.03023 |
| [21] | Parrilo, P.: Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. Ph.D. thesis, California Institute of Technology (2000) |
| [22] | Peyrl, H., Parrilo, P.A.: Computing sum of squares decompositions with rational coefficients. Theoretical Computer Science 409(2), 269–281 (2008) · Zbl 1156.65062 · doi:10.1016/j.tcs.2008.09.025 |
| [23] | Reznick, B.: Extremal PSD forms with few terms. Duke Mathematical Journal 45(2), 363–374 (1978) · Zbl 0395.10037 · doi:10.1215/S0012-7094-78-04519-2 |
| [24] | Reznick, B.: Some concrete aspects of Hilbert’s 17th problem. In: Delzell, C.N., Madden, J.J. (eds.) Real Algebraic Geometry and Ordered Structures, Contemporary Mathematics, vol. 253. American Mathematical Society, Providence (2000) · Zbl 0972.11021 |
| [25] | Safey El Din, M.: Computing the global optimum of a multivariate polynomial over the reals. In: ISSAC (International Symposium on Symbolic and Algebraic Computation), pp. 71–78. ACM, New York (2008) |
| [26] | Schweighofer, M.: On the complexity of Schmüdgen’s Positivstellensatz. Journal of Complexity 20(4), 529–543 (2004) · Zbl 1161.68480 · doi:10.1016/j.jco.2004.01.005 |
| [27] | Seidenberg, A.: A new decision method for elementary algebra. Annals of Mathematics 60(2), 365–374 (1954), http://www.jstor.org/stable/1969640 · Zbl 0056.01804 · doi:10.2307/1969640 |
| [28] | Stein, W.A.: Modular forms, a computational approach. Graduate studies in mathematics. American Mathematical Society, Providence (2007) |
| [29] | Stengle, G.: A Nullstellensatz and a Positivstellensatz in semialgebraic geometry. Mathematische Annalen 2(207), 87–87 (1973) · Zbl 0253.14001 |
| [30] | Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951) · Zbl 0044.25102 |
| [31] | Tiwari, A.: An algebraic approach for the unsatisfiability of nonlinear constraints. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 248–262. Springer, Heidelberg (2005) · Zbl 1136.68522 · doi:10.1007/11538363_18 |
| [32] | Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Review 38(1), 49–95 (1996) · Zbl 0845.65023 · doi:10.1137/1038003 |
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.
