Solving First-Order Constraints in the Theory of the Evaluated Trees | SpringerLink
Skip to main content
Springer Nature Link
Log in

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

  • Conference paper
Logic Programming (ICLP 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4079))

Included in the following conference series:

  • 477 Accesses

Abstract

We describe in this paper a general algorithm for solving first-order constraints 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. It transforms a first-order formula ϕ, which can possibly contain free variables, into a disjunction φ of solved formulas which is equivalent in T, without new free variables and such that φ is either \(\mathit{true}\) or \(\mathit{false}\) or a formula having at least one free variable and being equivalent neither to \(\mathit{true}\) nor to \(\mathit{false}\) in T.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Similar content being viewed by others

References

  1. Benhamou, F., et al.: Le manuel de Prolog IV, PrologIA, Marseille, France (1996)

    Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

  4. Dao, T.: Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis. Thèse d’informatique, Université de la Méditerranée (2000)

    Google Scholar 

  5. Dao, T.B.H., Djelloul, K.: Solving First-Order Constraints in the Theory of the Evaluated Trees, Rapport de recherche LIFO RR-2006-05, http://www.univ-orleans.fr/lifo/rapports.php

  6. Djelloul, K.: About the Combination of Trees and Rational Numbers in a Complete First-Order Theory. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 106–121. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

    Google Scholar 

  8. Vorobyov, S.: An Improved Lower Bound for the Elementary Theories of Trees. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 275–287. Springer, Heidelberg (1996)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIFO, Bat. 3IA, rue Léonard de Vinci, 45067, Orléans, France

    Thi-Bich-Hanh Dao

  2. LIF, Parc scientifique et technologique de Luminy, 13288, Marseille, France

    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

Editors and Affiliations

  1. University of Twente, The Netherlands

    Sandro Etalle

  2. Department of Computer Science, University of Kentucky, 40506, Lexington, KY, USA

    Mirosław Truszczyński

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dao, TBH., Djelloul, K. (2006). Solving First-Order Constraints in the Theory of the Evaluated Trees. In: Etalle, S., Truszczyński, M. (eds) Logic Programming. ICLP 2006. Lecture Notes in Computer Science, vol 4079. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11799573_32

Download citation

  • DOI: https://doi.org/10.1007/11799573_32

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-36635-5

  • Online ISBN: 978-3-540-36636-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation