Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm's and Tarski's Theorems

摘要

Sturm's theorem is a well-known result in real algebraic geometry that provides a function that computes the number of roots of a univariate polynomial in a semi-open interval, not counting multiplicity. A generalization of Sturm's theorem is known as Tarski's theorem, which provides a linear relationship between functions known as Tarski queries and cardinalities of certain sets. The linear system that results from this relationship is in fact invertible and can be used to explicitly count the number of roots of a univariate polynomial on a set defined by a system of polynomial relations. This paper presents a formalization of these results in the PVS theorem prover, including formal proofs of Sturm's and Tarski's theorems. These theorems are at the basis of two decision procedures, which are implemented as computable functions in PVS. The first, based on Sturm's theorem, determines satisfiability of a single polynomial relation over an interval. The second, based on Tarski's theorem, determines the satisfiability of a system of polynomial relations over the real line. The soundness and completeness properties of these decision procedures are formally verified in PVS. The procedures and their correctness properties enable the implementation of PVS strategies for automatically proving existential and universal statements on polynomial systems. Since the decision procedures are formally verified in PVS, the soundness of the strategies depends solely on the internal logic of PVS rather than on an external oracle.