Approximate Quantifiers for Solving First-Order Constraints

Title: Approximate Quantifiers for Solving First-Order Constraints

Abstract: This research proposes a method to solve first-order constraints over real numbers by introducing approximate quantifiers. These quantifiers allow for a trade-off between precision and efficiency, and they also introduce additional expressivity into the first-order language by allowing reasoning over the size of solution sets. The main contributions of this work are:

1. Demonstrating the need for exact intermediate computation in the proposed method. 2. Introducing approximate quantifiers with a positive real annotation and an interval annotation, which allow for a range of possible truth-values. 3. Proving that, from a good enough approximation of the solution sets of atomic sub-constraints, one can always compute at least one of the possible truth-values, allowing the computation of approximate solution sets with arbitrarily small error bounds.

The research presents a new method for solving first-order constraints over real numbers, which is completely domain-independent. It also discusses the concept of don't know and don't care nondeterminism, which arises in the proposed method due to the presence of several possible values for an object. The research concludes by stating that the proposed method can be easily extended to model other sources of nondeterminism.

Link to Article: https://arxiv.org/abs/0108013v1 Authors: arXiv ID: 0108013v1