L’algèbre des arbres finis ou infinis joue un rôle fondamental en informatique. Entre autres, le fonctionnement de Prolog II, III et IV a été modélisé par Alain Colmerauer comme la résolution de contraintes sous la forme d’équations et de diséquations dans cette algèbre. Dans un travail publié à la revue Constraints avec Alain Colmerauer [6], nous avons étudié l’expressivité des contraintes plus générales dans cette algèbre, qui sont des formules logiques du premier ordre, construites à partir des variables, désignant des arbres, d’opérations de construction, de la relation de l’égalité, des connecteurs logiques et des quantificateurs. Nous avons présenté la construction d’exemples pour montrer un pouvoir d’expressivité immensément grand de contraintes aussi générales. Cet article présente une version réduite de ce travail sur le pouvoir d’expressivité de ces contraintes [6]. De plus, nous décrivons la méthode que nous avons développée pour résoudre ces contraintes.
The algebra of finite or infinite trees plays a fundamental role in computer science. Among others, the execution of Prolog II, III and IV programs was modeled by Alain Colmerauer as solving constraints in the form of equations and disequations in this algebra. In a work published in the journal Constraints with Alain Colmerauer [6], we studied the expressiveness of more general constraints in this algebra, which are first-order logical formulas, constructed using variables designating trees, construction operations, the equality relation, logical connectors and quantifiers. We have presented examples to show an immense expressivity power of such general constraints. This paper presents a reduced version of this work on the expressiveness of these constraints [6]. Moreover, we describe the method we have developed to solve such constraints.
Accepté le :
Publié le :
Keywords: Tree algebra, Constraints, Expressiveness of constraint, Constraint solving.
Thi-Bich-Hanh Dao 1
CC-BY 4.0
@article{ROIA_2024__5_2-3_121_0,
author = {Thi-Bich-Hanh Dao},
title = {Contraintes du premier ordre dans l{\textquoteright}alg\`ebre des arbres finis ou infinis},
journal = {Revue Ouverte d'Intelligence Artificielle},
pages = {121--138},
publisher = {Association pour la diffusion de la recherche francophone en intelligence artificielle},
volume = {5},
number = {2-3},
year = {2024},
doi = {10.5802/roia.75},
language = {fr},
url = {https://roia.centre-mersenne.org/articles/10.5802/roia.75/}
}
TY - JOUR AU - Thi-Bich-Hanh Dao TI - Contraintes du premier ordre dans l’algèbre des arbres finis ou infinis JO - Revue Ouverte d'Intelligence Artificielle PY - 2024 SP - 121 EP - 138 VL - 5 IS - 2-3 PB - Association pour la diffusion de la recherche francophone en intelligence artificielle UR - https://roia.centre-mersenne.org/articles/10.5802/roia.75/ DO - 10.5802/roia.75 LA - fr ID - ROIA_2024__5_2-3_121_0 ER -
%0 Journal Article %A Thi-Bich-Hanh Dao %T Contraintes du premier ordre dans l’algèbre des arbres finis ou infinis %J Revue Ouverte d'Intelligence Artificielle %D 2024 %P 121-138 %V 5 %N 2-3 %I Association pour la diffusion de la recherche francophone en intelligence artificielle %U https://roia.centre-mersenne.org/articles/10.5802/roia.75/ %R 10.5802/roia.75 %G fr %F ROIA_2024__5_2-3_121_0
Thi-Bich-Hanh Dao. Contraintes du premier ordre dans l’algèbre des arbres finis ou infinis. Revue Ouverte d'Intelligence Artificielle, Volume 5 (2024) no. 2-3, pp. 121-138. doi : 10.5802/roia.75. https://roia.centre-mersenne.org/articles/10.5802/roia.75/
[1] Le manuel de Prolog IV (1996)
[2] Solving disequations in equational theories, Proc. 9th Conf. on Automated Deduction (LNCS 310), Springer-Verlag (1988), pp. 517-526 | DOI | Zbl
[3] Prolog and Infinite Trees, Logic Programming (K. L. Clark; S.-A. Tarnlund, eds.), Academic Press, New York (1982), pp. 231-251
[4] Equations and Inequations on Finite and Infinite Trees, Proceeding of the International Conference on Fifth Generation Computer Systems (FCGS-84), Tokyo, ICOT (1984), pp. 85-99
[5] An Introduction to Prolog III, Communications of the ACM, Volume 33 (1990) no. 7, pp. 68-90 | DOI
[6] Expressiveness of Full First-Order Constraints in the Algebra of Finite or Infinite Trees, Constraints, Volume 8 (2003) no. 3, pp. 283-302 | DOI | Zbl
[7] Prolog, Theoretical Principles and Current Trends, Technology and Science of Informatics, Volume 2 (1983) no. 4, pp. 255-292 (Version anglaise de la revue TSI, AFCET-Bordas)
[8] Disunification : a Survey, Computational Logic : Essays in Honor of Alan Robinson (J.L. Lassez; G. Plotkin, eds.), MIT Press, 1991
[9] Résolution de contraintes dans des algèbres de termes (1992) (Rapport d’Habilitation)
[10] Equational Problems and Disunification, Journal of Symbolic Computation, Volume 7 (1989) no. 3-4, pp. 371-425 | DOI | Zbl
[11] Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis, Thèse d’Informatique, Université Aix-Marseille 2 (2000)
[12] Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis, Programmation en logique avec contraintes, JFPLC 2000, 28-30 Juin 2000, Marseille, France (Touraïvane, ed.), Hermes (2000), pp. 225-240
[13] Theory of finite or infinite trees revisited, Theory Pract. Log. Program., Volume 8 (2008) no. 4, pp. 431-489 | DOI | Zbl
[14] Résolution d’équations dans les langages d’ordre , Thèse d’État, Université Paris 7 (1976)
[15] Efficient unification over infinite terms, New Generation Computing, Volume 2 (1984) no. 3, pp. 207-219 | DOI
[16] Solving Equations in Abstract algebras : A Rule-Based survey of unifications, Computational Logic : Essays in Honor of Alan Robinson (J.L. Lassez; G. Plotkin, eds.), MIT Press (1991), pp. 257-331
[17] Negation in Logic Programming, Journal of Logic Programming, Volume 4 (1987), pp. 289-308 | DOI | Zbl
[18] Complete Axiomatization of the Algebra of Finite, Rational and Infinite Trees (1988) (Technical report)
[19] Axiomatizable classes of locally free algebras of various types, The Metamathematics of Algebraic Systems. Anatolii Ivanovic Malcev. Collected Papers : 1936-1967 (B. Wells III, ed.), Volume 66, North Holland, 1971, pp. 262-281
[20] Basic theory of feature trees, ACM Trans. Comput. Log., Volume 5 (2004) no. 3, pp. 385-402 | DOI | Zbl
[21] Incremental algorithms for constraint solving and entailment over rational trees, Proc. of the 13th Conference Foundations of Software Technology and Theoretical Computer Science (LNCS), Volume 761 (1993), pp. 205-217 | DOI
[22] A machine-oriented logic based on the resolution principle, JACM, Volume 12 (1965) no. 1, pp. 23-41 | DOI | Zbl
[23] Constraint operations for , Logic Programming : Proceedings of the 8th International Conference, Paris (1991), pp. 760-774
[24] An Improved Lower Bound for the Elementary Theories of Trees, Proceeding of the 13th International Conference on Automated Deduction, CADE’96 (Lecture Notes in Artificial Intelligence), Volume 1104, Springer (1996), pp. 275-287 | DOI | Zbl
Cité par Sources :