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

Authors

  • Anthony Joseph Narkawicz NASA Langley Research Center, Bldg. 1220, Room 115 MS. 130, Hampton, VA 23681-2199, USA
  • Cesar Munoz NASA Langley Research Center, Bldg. 1220, Room 115 MS. 130, Hampton, VA 23681-2199, USA
  • Aaron M. Dutle NASA Langley Research Center, Bldg. 1220, Room 115 MS. 130, Hampton, VA 23681-2199, USA

DOI:

https://doi.org/10.6092/issn.1972-5787/8212

Keywords:

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

Abstract

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.

Downloads

Published

2018-05-29

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

Issue

Section

Articles