Loading...
Please wait, while we are loading the content...
Similar Documents
Solving First-Order Constraints in the Theory of the Evaluated Trees
| Content Provider | CiteSeerX |
|---|---|
| Author | Dao, Thi-Bich-Hanh Djelloul, Khalil |
| Abstract | Abstract. We present in this paper a first-order extension of the solver of Prolog III, by giving not only a decision procedure, but a full firstorder constraint solver in the theory T of the evaluated trees, which is a combination of the theory of finite or infinite trees and the theory of the rational numbers with addition, subtraction and a linear dense order relation. The solver is given in the form of 28 rewriting rules which transform any first-order formula ϕ into an equivalent disjunction φ of simple formulas in which the solutions of the free variables are expressed in a clear and explicit way. The correctness of our algorithm implies the completeness of a first-order theory built on the model of Prolog III. 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Decision Procedure Free Variable Infinite Tree Equivalent Disjunction First-order Formula Simple Formula First-order Extension First-order Theory Rewriting Rule Rational Number Evaluated Tree Full Firstorder Constraint Solver Prolog Iii Linear Dense Order Relation Explicit Way First-order Constraint |
| Content Type | Text |
| Resource Type | Article |
