Narkawicz Anthony, Munoz Cesar, Dutle Aaron
NASA Langley Research Center, Hampton, VA 23681-2199.
J Formaliz Reason. 2018;11(1):19-41. doi: 10.6092/issn.1972-5787/8212.
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.
本文提出了一种经过形式验证的判定过程，用于确定实直线上一元多项式关系系统的可满足性。该过程将基于施图姆定理的根计数函数与区间细分算法相结合。给定一个关于同一变量的多项式关系系统，判定过程将实区间逐步细分为更小的区间。细分过程持续进行，直到可以使用该系统部分多项式上的施图姆定理在每个子区间上确定系统的可满足性。该判定过程已在原型验证系统（PVS）中进行了形式验证。在PVS中，判定过程被指定为多项式关系深度嵌入上的可计算布尔函数。此函数用于定义一种证明生成策略，用于自动证明多项式系统上的存在性和全称性陈述。该策略的可靠性仅取决于PVS的内部逻辑。
