NTRS - NASA Technical Reports Server

Back to Results
a formally-verified decision procedure for univariate polynomial computation based on sturm's theoremSturm'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 semiopen interval. This paper presents a formalization of this theorem in the PVS theorem prover, as well as a decision procedure that checks whether a polynomial is always positive, nonnegative, nonzero, negative, or nonpositive on any input interval. The soundness and completeness of the decision procedure is proven in PVS. The procedure and its correctness properties enable the implementation of a PVS strategy for automatically proving existential and universal univariate polynomial inequalities. Since the decision procedure is formally verified in PVS, the soundness of the strategy depends solely on the internal logic of PVS rather than on an external oracle. The procedure itself uses a combination of Sturm's Theorem, an interval bisection procedure, and the fact that a polynomial with exactly one root in a bounded interval is always nonnegative on that interval if and only if it is nonnegative at both endpoints.
Document ID
Document Type
Technical Memorandum (TM)
Narkawicz, Anthony J.
(NASA Langley Research Center Hampton, VA, United States)
Munoz, Cesar A.
(NASA Langley Research Center Hampton, VA, United States)
Date Acquired
February 3, 2015
Publication Date
November 1, 2014
Subject Category
Theoretical Mathematics
Report/Patent Number
Funding Number(s)
WBS: WBS 534723.02.15.07
Distribution Limits
Work of the US Gov. Public Use Permitted.

Available Downloads

NameType 20150001256.pdf STI