Semantics of Division for Polynomial Solvers

TL;DR

This paper tackles the challenging problem of handling division in first-order real-closed-shaped formulas within polynomial solvers. It introduces fair-SAT as a semantics that captures division behavior without fixating on a single divide-by-zero convention, and defines the concept of well-defined formulas to decide when naive denominator clearing preserves meaning. A translation algorithm translate(F) is developed to convert division-containing formulas into purely polynomial constraints, preserving fair-SAT for non-well-defined cases and equivalence to the naive polynomial form for well-defined cases; key notions include partial evaluation and the use of U_i/V_i guards to manage undefined divisions. The work provides rigorous proofs of properties such as preservation of fair-SAT under logical rewritings and quantifier handling and demonstrates an implementation in the Tarski system, suggesting a principled, practically viable path for computer algebra solvers while clarifying scope for SMT/theorem-proving contexts. Overall, the paper delivers a formal, implementable framework for division semantics in quantified polynomial constraints with concrete definitions, proofs, and a working translation pipeline.

Abstract

How to handle division in systems that compute with logical formulas involving what would otherwise be polynomial constraints over the real numbers is a surprisingly difficult question. This paper argues that existing approaches from both the computer algebra and computational logic communities are unsatisfactory for systems that consider the satisfiability of formulas with quantifiers or that perform quantifier elimination. To address this, we propose the notion of the fair-satisfiability of a formula, use it to characterize formulas with divisions that are well-defined, meaning that they adequately guard divisions against division by zero, and provide a translation algorithm that converts a formula with divisions into a purely polynomial formula that is satisfiable if and only if the original formula is fair-satisfiable. This provides a semantics for division with some nice properties, which we describe and prove in the paper.

Figures (2)

• Figure 1: The figure on the left is the set of $(z,y)$-values satisfying $F'_1$. The figure on the right is the set of $z,y$-values satisfying the $x \neq 0$ branch of formula $F'_1$, which corresponds to guarding against division by zero and clearing denominators in $F_1$, but without adding the extra branch introduced by defining $y/0$ to be zero. The half-ellipse cut out in the right figure corresponds to $x = 0$, i.e. where the denominator vanishes, which has been disallowed. In the left figure, some but not all of that ellipse has been introduce into the solution. The reason part of the ellipse is cut out is that a new constraint, $8 y \leq 8 - (z + y + 1)^2$, is introduced by defining $y/0=0$. This is a constraint (and, underlying it, a polynomial) that in usual mathematical practice has no connection to the original problem.
• Figure 2: Tarski session using the formula from Example \ref{['ex:nullmatters']} and example input from Section \ref{['section:capractice']}

Theorems & Definitions (42)

• Definition 1
• Definition 2: partial evaluation of a term
• Definition 3: p-evaluation extended to tuples
• Definition 4
• Definition 5: partial evaluation of a formula
• Definition 6
• Definition 7
• Definition 8: fair-SAT
• Definition 9: fair-SAT equivalence
• Example 1