Convergent Approximate Solving of First-Order Constraints by Approximate Quantifiers

摘要

Exactly solving first-order constraints (i.e., first-order formulas over acertain predefined structure) can be a very hard, or even undecidable problem.In continuous structures like the real numbers it is promising to computeapproximate solutions instead of exact ones. However, the quantifiers of thefirst-order predicate language are an obstacle to allowing approximations toarbitrary small error bounds. In this paper we solve the problem by modifyingthe first-order language and replacing the classical quantifiers withapproximate quantifiers. These also have two additional advantages: First, theyare tunable, in the sense that they allow the user to decide on the trade-offbetween precision and efficiency. Second, they introduce additionalexpressivity into the first-order language by allowing reasoning over the sizeof solution sets.