Increasing Model Building Capabilities by Constraint Solving on Terms with Integer Exponents
✍ Scribed by NICOLAS PELTIER
- Publisher
- Elsevier Science
- Year
- 1997
- Tongue
- English
- Weight
- 770 KB
- Volume
- 24
- Category
- Article
- ISSN
- 0747-7171
No coin nor oath required. For personal study only.
✦ Synopsis
We extend a former method for simultaneous search for refutations and models, based on the use of constraints, by extending the expressive power of the constraints. Our extension uses the language of I-terms, in which it is possible to denote infinite sequences of structurally similar terms. Our work generalizes the results of Comon (1995). Comon gives only a unification algorithm for "one hole" I-terms, while we present a decision procedure for term constraints with integer exponents (only decidability of the positive existential fragment was known so far).
We show that the formalism of I-terms can be profitably integrated into our method for model building. In particular, it allows us to specify all the resolvents of some kinds of self-resolvent clauses. This feature is especially useful in model building. We illustrate our approach with two non-trivial examples, showing that the extension presented here increases the power of our method, i.e. the class of formulae for which it is able to build models.