Formalization of Sturm's Theorem
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. The PVS
contribution Sturm, which is part of the NASA PVS Library,
includes a formalization of Sturm's Theorem, as well as a decision
procedure that determines the sign of a univariate polynomial on a
given interval. The decision procedure uses a combination of Sturm's
Theorem, an interval bisection procedure, and the fact that a
polynomial with exactly one root in a finite interval is always
nonnegative on that interval if and only if it is nonnegative at both
endpoints. It is formally verified in PVS that the
decision procedure is sound and complete.
This result is a the basis of the proof-producing
strategies sturm and mono-poly for reasoning about polynomial relations over a real
interval. The soundness of the strategies depends solely on the internal logic of PVS
rather than on an external oracle.
PVS Contribution
sturm: Automatically discharges polynomial relations over a real interval.mono-poly: Automaically discharges monocity properties of polynomials on a real interval.Publications
- Anthony Narkawicz, César Muñoz, and Aaron Dutle,
Formally-Verified Decision Procedures for Univariate Polynomial
Computation Based on Sturm’s and Tarski’s Theorems, Journal
of Automated Reasoning, Volume 54, Issue 4, pp. 285-326, 2015. DOI: 10.1007/s10817-015-9320-x. BibTeX
Reference.
- Anthony Narkawicz and César Muñoz, A Formally Verified Conflict Detection Algorithm for Polynomial Trajectories, Proceedings of the 2015 AIAA Infotech @ Aerospace Conference, AIAA-2015-0795, Kissimmee, Florida, 2015. BibTeX Reference.
- Anthony Narkawicz and César Muñoz, A Formally-Verified Decision Procedure for Univariate Polynomial Computation Based on Sturm’s Theorem, Technical Memorandum, NASA/TM-2014-218548, November 2014. BibTeX Reference.
identifies links that are outside
the NASA domain
