Contraintes du premier ordre dans l’algèbre des arbres finis ou infinis
Revue Ouverte d'Intelligence Artificielle, Hommage à Alain Colmerauer, Volume 5 (2024) no. 2-3, pp. 121-138.

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.

Reçu le :
Accepté le :
Publié le :
DOI : 10.5802/roia.75
Mot clés : Algèbre des arbres, contraintes, expressivité de contraintes, résolution de contraintes.
Keywords: Tree algebra, Constraints, Expressiveness of constraint, Constraint solving.

Thi-Bich-Hanh Dao 1

1 Univ. Orléans, INSA Centre Val de Loire, LIFO EA 4022, F-45067, Orléans (France)
Licence : CC-BY 4.0
Droits d'auteur : Les auteurs conservent leurs droits
@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, Hommage à Alain Colmerauer, 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] F. Benhamou; P. Bouvier; A. Colmerauer; H. Garetta; B. Giletta; J.L. Massat; G.A. Narboni; S. N’Dong; R. Pasero; J.F. Pique; Touraïvane; M. Van Caneghem; E. Vétillard Le manuel de Prolog IV (1996)

[2] Hans-Jurgen Bürckert Solving disequations in equational theories, Proc. 9th Conf. on Automated Deduction (LNCS 310), Springer-Verlag (1988), pp. 517-526 | DOI | Zbl

[3] Alain Colmerauer Prolog and Infinite Trees, Logic Programming (K. L. Clark; S.-A. Tarnlund, eds.), Academic Press, New York (1982), pp. 231-251

[4] Alain Colmerauer 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] Alain Colmerauer An Introduction to Prolog III, Communications of the ACM, Volume 33 (1990) no. 7, pp. 68-90 | DOI

[6] Alain Colmerauer; Thi-Bich-Hanh Dao 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] Alain Colmerauer; Henri Kanoui; Michel Van Caneghem 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] Hubert Comon Disunification : a Survey, Computational Logic : Essays in Honor of Alan Robinson (J.L. Lassez; G. Plotkin, eds.), MIT Press, 1991

[9] Hubert Comon Résolution de contraintes dans des algèbres de termes (1992) (Rapport d’Habilitation)

[10] Hubert Comon; Pierre Lescanne Equational Problems and Disunification, Journal of Symbolic Computation, Volume 7 (1989) no. 3-4, pp. 371-425 | DOI | Zbl

[11] Thi-Bich-Hanh Dao 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] Thi-Bich-Hanh Dao 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] Khalil Djelloul; Thi-Bich-Hanh Dao; Thom W. Frühwirth Theory of finite or infinite trees revisited, Theory Pract. Log. Program., Volume 8 (2008) no. 4, pp. 431-489 | DOI | Zbl

[14] Gérard Huet Résolution d’équations dans les langages d’ordre 1,2,...,ω, Thèse d’État, Université Paris 7 (1976)

[15] Joxan Jaffar Efficient unification over infinite terms, New Generation Computing, Volume 2 (1984) no. 3, pp. 207-219 | DOI

[16] Jean-Pierre Jouannaud; Claude Kirchner 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] Kenneth Kunen Negation in Logic Programming, Journal of Logic Programming, Volume 4 (1987), pp. 289-308 | DOI | Zbl

[18] Michael J. Maher Complete Axiomatization of the Algebra of Finite, Rational and Infinite Trees (1988) (Technical report)

[19] Anatolii Malcev 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] Pawel Mielniczuk Basic theory of feature trees, ACM Trans. Comput. Log., Volume 5 (2004) no. 3, pp. 385-402 | DOI | Zbl

[21] Viswanath Ramachandran; Pascal Van Hentenryck 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] J.A. Robinson A machine-oriented logic based on the resolution principle, JACM, Volume 12 (1965) no. 1, pp. 23-41 | DOI | Zbl

[23] Donald A. Smith Constraint operations for CLP(ℱ𝒯), Logic Programming : Proceedings of the 8th International Conference, Paris (1991), pp. 760-774

[24] Sergei Vorobyov 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 :