A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision
Keywords:Univariate polynomials, satisfiability, Sturm's theorem, Prototype Verification System, PVS, deep embedding
AbstractThis paper presents a formally verified decision procedure for determinining the satisfiability of a system of univariate polynomial relations over the real line. The procedure combines a root counting function, based on Sturm’s theorem, with an interval subdivision algorithm. Given a system of polynomial relations over the same variable, the decision procedure progressively subdivides the real interval into smaller intervals. The subdivision continues until the satisfiability of the system can be determined on each subinterval using Sturm’s theorem on a subset of the system’s polynomials. The decision procedure has been formally verified in the Prototype Verification System (PVS). In PVS, the decision procedure is specified as a computable Boolean function on a deep embedding of polynomial relations. This function is used to define a proof producing strategy for automatically proving existential and universal statements on polynomial systems. The soundness of the strategy solely depends on the internal logic of PVS.
How to Cite
Narkawicz, A. J., Munoz, C., & Dutle, A. M. (2018). A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision. Journal of Formalized Reasoning, 11(1), 19–41. https://doi.org/10.6092/issn.1972-5787/8212
Copyright (c) 2018 Cesar Munoz, Anthony Joseph Narkawicz, Aaron M. Dutle
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.