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 first-order 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Benhamou, F., Van Caneghem, M.C.: Le manuel de Prolog IV, PrologIA, France (1996)
Bürckert, H.: Solving disequations in equational theories. In: Lusk, E.‘., Overbeek, R. (eds.) 9th International Conference on Automated Deduction. LNCS, vol. 310, pp. 517–526. Springer, Heidelberg (1988)
Colmerauer, A.: An introduction to Prolog III. Communication of the ACM 33(7), 68–90 (1990)
Colmerauer, A.: Equations and disequations on finite and infinite trees. In: Proc of the 5th conf on generation of computer systems Tokyo, 1984, pp. 85–99 (1984)
Colmerauer, A.: Prolog and infinite trees. In: Clark, K.L., Tarnlund, S-A. (eds.) Logic Programming, pp. 231–251. Academic Press, London (1982)
Comon, H.: Résolution de contraintes dans des algèbres de termes. Rapport d’Habilitation, Université de Paris Sud (1992)
Courcelle, B.: Fundamental Properties of Infinite Trees. TCS 25(2), 95–169 (1983)
Dao, T., Djelloul, K.: Solving first-order constraints in evaluated trees. Technical report, Laboratoire d’informatique fondamentale d’Orlans, RR-2006-05, Full version of this paper with full proofs, http://www.univ-orleans.fr/lifo/rapports.php
Djelloul, K.: About the combination of trees and rational numbers in a complete first-order theory. In: Gramlich, B. (ed.) Frontiers of Combining Systems. LNCS (LNAI), vol. 3717, pp. 106–122. Springer, Heidelberg (2005)
Djelloul, K., Dao, T.: Solving First-Order formulas in the Theory of Finite or Infinite Trees. In: SAC 2006. Proceeding of the 21st ACM Symposium on Applied Computing, pp. 7–14. ACM Press, New York (2006)
Djelloul, K., Dao, T.: Extension into trees of first order theories. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol. 4120, pp. 53–67. Springer, Heidelberg (2006)
Djelloul, K.: Decomposable Theories. Journal of Theory and practice of Logic Programming (to appear)
Huet, G.: Resolution d’equations dans les langages d’ordre 1, 2,...ω. These d’Etat, Universite Paris 7. France (1976)
Jaffar, J.: Efficient unification over infinite terms. New Generation Computing 2(3), 207–219 (1984)
Jouannaud, J.P., Kirchner, C.: Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. Computational Logic - Essays in Honor of Alan Robinson, pp. 257–321. MIT Press, Cambridge (1991)
Lassez, J., Maher, M., Marriott, K.: Unification revisited. In: proceedings of the workshop on the foundations of deductive database and logic programming, pp. 587–625 (1986)
Lassez, J., Marriott, K.: Explicit representation of terms defined by counter examples. Journal of automated reasonning. 3, 301–317 (1987)
Lassez, J., McAloon, K.: Independence of negative constraints. In: Díaz, J., Orejas, F. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol. 351, pp. 19–27. Springer, Heidelberg (1989)
Maher, M.: Complete axiomatization of the algebra of finite, rational and infinite trees. Technical report, IBM - T.J.Watson Research Center (1988)
Maher, M., Stuckey, P.: On inductive inference of cyclic structures. Annals of mathematics and artificial intelligence 15(2), 167–208 (1995)
Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. on Languages and Systems 4(2), 258–282 (1982)
Paterson, M., Wegman, N.: Linear unification. Journal of Computer and Systems Science 16, 158–167 (1978)
Ramachandran, V., Van Hentenryck, P.: Incremental algorithms for constraint solving and entailment over rational trees. In: Shyamasundar, R.K. (ed.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 761, pp. 205–217. Springer, Heidelberg (1993)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. JACM 12(1), 23–41 (1965)
Vorobyov, S.: An Improved Lower Bound for the Elementary Theories of Trees. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction - Cade-13. LNCS, vol. 1104, pp. 275–287. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dao, TBH., Djelloul, K. (2007). Solving First-Order Constraints in the Theory of the Evaluated Trees. In: Azevedo, F., Barahona, P., Fages, F., Rossi, F. (eds) Recent Advances in Constraints. CSCLP 2006. Lecture Notes in Computer Science(), vol 4651. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73817-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-73817-6_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73816-9
Online ISBN: 978-3-540-73817-6
eBook Packages: Computer ScienceComputer Science (R0)