TY - JOUR
AU - Narkawicz, Anthony Joseph
AU - Munoz, Cesar
AU - Dutle, Aaron M.
PY - 2018/01/01
Y2 - 2022/12/04
TI - A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision
JF - Journal of Formalized Reasoning
JA - JFR
VL - 11
IS - 1
SE - Articles
DO - 10.6092/issn.1972-5787/8212
UR - https://jfr.unibo.it/article/view/8212
SP - 19 - 41
AB - This 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.
ER -