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.

翻译：在涉及实数域多项式约束的逻辑公式计算系统中如何处理除法是一个异常困难的问题。本文认为，无论是计算机代数领域还是计算逻辑领域现有的方法，对于考虑带量词公式可满足性或执行量词消去的系统而言都存在不足。为此，我们提出公式的公平可满足性概念，利用该概念刻画具有良定义性的含除法公式（即能充分防范除零操作），并提供一种翻译算法，可将含除法的公式转换为纯多项式公式，且该多项式公式可满足当且仅当原公式具有公平可满足性。这为除法提供了一种具有良好性质的语义，我们在文中对这些性质进行了描述和证明。