Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Constraint Solving and Constraint Logic Programming

CSCLP 2006: Recent Advances in Constraints pp 108–123Cite as

Solving First-Order Constraints in the Theory of the Evaluated Trees

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4651))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Benhamou, F., Van Caneghem, M.C.: Le manuel de Prolog IV, PrologIA, France (1996)

    Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Colmerauer, A.: An introduction to Prolog III. Communication of the ACM 33(7), 68–90 (1990)

    Article  Google Scholar 

  4. 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)

    Google Scholar 

  5. Colmerauer, A.: Prolog and infinite trees. In: Clark, K.L., Tarnlund, S-A. (eds.) Logic Programming, pp. 231–251. Academic Press, London (1982)

    Google Scholar 

  6. Comon, H.: Résolution de contraintes dans des algèbres de termes. Rapport d’Habilitation, Université de Paris Sud (1992)

    Google Scholar 

  7. Courcelle, B.: Fundamental Properties of Infinite Trees. TCS 25(2), 95–169 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  8. 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

  9. 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)

    Chapter  Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. Djelloul, K.: Decomposable Theories. Journal of Theory and practice of Logic Programming (to appear)

    Google Scholar 

  13. Huet, G.: Resolution d’equations dans les langages d’ordre 1, 2,...ω. These d’Etat, Universite Paris 7. France (1976)

    Google Scholar 

  14. Jaffar, J.: Efficient unification over infinite terms. New Generation Computing 2(3), 207–219 (1984)

    Article  MathSciNet  Google Scholar 

  15. 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)

    Google Scholar 

  16. 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)

    Google Scholar 

  17. Lassez, J., Marriott, K.: Explicit representation of terms defined by counter examples. Journal of automated reasonning. 3, 301–317 (1987)

    MATH  MathSciNet  Google Scholar 

  18. 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)

    Google Scholar 

  19. Maher, M.: Complete axiomatization of the algebra of finite, rational and infinite trees. Technical report, IBM - T.J.Watson Research Center (1988)

    Google Scholar 

  20. Maher, M., Stuckey, P.: On inductive inference of cyclic structures. Annals of mathematics and artificial intelligence 15(2), 167–208 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  21. Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. on Languages and Systems 4(2), 258–282 (1982)

    Article  MATH  Google Scholar 

  22. Paterson, M., Wegman, N.: Linear unification. Journal of Computer and Systems Science 16, 158–167 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  23. 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)

    Google Scholar 

  24. Robinson, J.A.: A machine-oriented logic based on the resolution principle. JACM 12(1), 23–41 (1965)

    Article  MATH  Google Scholar 

  25. 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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d’Informatique Fondamentale d’Orléans, France

    Thi-Bich-Hanh Dao

  2. Faculty of Computer Science, University of Ulm, Germany

    Khalil Djelloul

Authors
  1. Thi-Bich-Hanh Dao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Khalil Djelloul
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Francisco Azevedo Pedro Barahona François Fages Francesca Rossi

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation