Abstract
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.
This work was partially supported by ANR project “ASOPT”.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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)
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)
Benson, S.J., Ye, Y.: DSDP5 user guide — software for semidefinite programming. technical memorandum 277. Argonne National Laboratory (2005)
Benson, S.J., Ye, Y.: Algorithm 875: DSDP5—software for semidefinite programming. ACM Transactions on Mathematical Software 34(3), 16:1–16:20 (2008)
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)
Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004), http://www.stanford.edu/~boyd/cvxbook/
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)
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)
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)
Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Tech. Rep. SRI-CSL-06-01, SRI International (May 2006)
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)
INRIA: The Coq Proof Assistant Reference Manual, 8.1 edn. (2006)
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)
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
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)
Krivine, J.L.: Anneaux préordonnés. J. Analyse Math. 12, 307–326 (1964), http://hal.archives-ouvertes.fr/hal-00165658/en/
Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008)
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
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)
Mahboubi, A.: Implementing the CAD algorithm inside the Coq system. Mathematical Structures in Computer Sciences 17(1) (2007)
Parrilo, P.: Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. Ph.D. thesis, California Institute of Technology (2000)
Peyrl, H., Parrilo, P.A.: Computing sum of squares decompositions with rational coefficients. Theoretical Computer Science 409(2), 269–281 (2008)
Reznick, B.: Extremal PSD forms with few terms. Duke Mathematical Journal 45(2), 363–374 (1978)
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)
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)
Schweighofer, M.: On the complexity of Schmüdgen’s Positivstellensatz. Journal of Complexity 20(4), 529–543 (2004)
Seidenberg, A.: A new decision method for elementary algebra. Annals of Mathematics 60(2), 365–374 (1954), http://www.jstor.org/stable/1969640
Stein, W.A.: Modular forms, a computational approach. Graduate studies in mathematics. American Mathematical Society, Providence (2007)
Stengle, G.: A Nullstellensatz and a Positivstellensatz in semialgebraic geometry. Mathematische Annalen 2(207), 87–87 (1973)
Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951)
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)
Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Review 38(1), 49–95 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Monniaux, D., Corbineau, P. (2011). On the Generation of Positivstellensatz Witnesses in Degenerate Cases. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds) Interactive Theorem Proving. ITP 2011. Lecture Notes in Computer Science, vol 6898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22863-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-22863-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22862-9
Online ISBN: 978-3-642-22863-6
eBook Packages: Computer ScienceComputer Science (R0)