A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision

Cesar Munoz, Anthony Joseph Narkawicz, Aaron M. Dutle


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.


Univariate polynomials; satisfiability; Sturm's theorem; Prototype Verification System; PVS; deep embedding

Full Text:

PDF (English)

DOI: 10.6092/issn.1972-5787/8212

Copyright (c) 2018 Cesar Munoz, Anthony Joseph Narkawicz, Aaron M. Dutle

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.