Reseña: Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems
Se ha publicado un artículo de razonamiento formalizado en PVS titulado Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems
Sus autores son Anthony Narkawicz, César Muñoz y Aaron M. Dutle (del Formal Methods group en el NASA Langley Research Center).
Su resumen es
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.
El trabajo se publicará en el Journal of Automated Reasoning.
El código de las correspondientes teorías en PVS del teorema de Sturm se encuentra aquí y el del teorema de Tarski aquí.