From decomposable to residual theories

摘要

Over the last decade, first-order constraints have been efficiently used in the artificial intelligence world to model many kinds of complex problems such as: scheduling, resource allocation, computer graphics and bio-informatics. Recently, a new property called decomposability has been introduced and many first-order theories have been proved to be decomposable: finite or infinite trees, rational and real numbers, linear dense order, etc. A decision procedure in the form of five rewriting rules has also been developed. This latter can decide if a first-order formula without free variables is true or not in any decomposable theory. Unfortunately, the definition of decomposable theories is too much complex: theoretical and definitively not intuitive. As a consequence, checking whether a given theory T is decomposable is almost impossible for a non expert in decomposability. We introduce in this paper residual theories: a new class of first-order theories whose definition is very intuitive, easy to check and much more adapted to the needs of the artificial intelligence community. We show that decomposable theories is a sub-class of residual theories and present, not only a decision procedure, but a full first-order constraint solver for residual theories. It transforms any first-order constraint φ (which can possibly contain free variables) into an equivalent formula ϕ which is either the formula true, or the formula false or a simple solved formula having at least one free variable and being equivalent neither to true nor to false. We show the efficiency of our solver by solving complex first-order constraints containing long nested alternations of quantifiers over different residual theories.