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.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Benhamou, F., et al.: Le manuel de Prolog IV, PrologIA, Marseille, France (1996)
Colmerauer, A.: An introduction to Prolog III. Comm. of the ACM 33(7), 68–90 (1990)
Comon, H.: Résolution de contraintes dans des algèbres de termes. Rapport d’Habilitation, Université de Paris Sud (1992)
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)
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
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)
Maher, M.: Complete axiomatization of the algebra of finite, rational and infinite trees. Technical report, IBM - T.J.Watson Research Center (1988)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)