A. Appendice and . Preuves-de-complétude-manière, Cependant, cela signifie que les atomes (WI[T2] ~ v) et (w} [Tl] ~ v) sont interprétés différemment, ce qui n'est possible (par construction de l'arbre sémantique) que si l'atome (WI ~ v) n'est pas réductible par (l~ ~ T2)' c'est-A-dire si (l~ ~ T2) > (WI ~ v)

. Dans-la-suite-de-la-preuve, nous allons étudier l'extension (12 ~ T2)' Mais, pour faire le lien avec le terme w}, il faut montrer que K( WI Nous allons montrer que cette restriction

. En, et T 2 ne sont pas E-égaux, au vu des preuves des Lemmes 3.2 et 3.3 (E-fermeture locale et E-fermeture de la relation --tCle E), la E-fermeture du graphe 2' précédent ne peut être réalisée que de deux manières: ? Soit A l'aide d'une réduction au

E. Un-terme and A. Wi, Comme nous étudions le cas A WI[T2] et T2 ne sont pas E-égaux, le contexte (e~, o~) utilisé dans la réduction précédente est un vrai contexte

~. Si-le-contexte and . D~ct, 1 2 = h, une E-paramodulation contextuelle de C~CT dans C~CT, avec le contexte (e~, o~), engendre une clause E-égale A (e~

@. Soit and A. , une réduction dans un sous-terme strict de 1 2 , correspondant A l'occurrence d'une variable lors d'une étape de E-égalité entre Wl et 1 2 (Cas 3(b)i) Le terme déduit est E-égal A WI[T 2 ] (propriétés de l'ordre sur les termes) Dans ce cas, nous pouvons étudier la E-fermeture du graphe formé par cette réduction et la E-égalité entre 1 2 et le sous

J. [. Anantharaman, J. Hsiang, and . Mzali, SbReve2: A term rewriting laboratory with (AC)-unfailing completion, Proceedings 3rd Conference on Rewriting Techniques Applications, pp.533-537, 1986.
DOI : 10.1007/3-540-51081-8_131

P. [. Cherifa and . Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming, vol.9, issue.2, pp.137-160, 1987.
DOI : 10.1016/0167-6423(87)90030-X

URL : https://hal.archives-ouvertes.fr/inria-00075876

N. Dershowitz, Completion for Rewriting Modulo a Congruence, Theoretical Computer Science, vol.67, issue.2-3, pp.173-202, 1989.

H. Bachmair and . Ganzinger, On restrictions of ordered paramodulation with simplification, Proceedings 10th International Conference on Automated Deduction, pp.427-441, 1990.
DOI : 10.1007/3-540-52885-7_105

H. [. Bachmair and . Ganzinger, Associative-commutative superposition, 1993.
DOI : 10.1007/3-540-60381-6_1

H. [. Bachmair and . Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.1-31, 1994.
DOI : 10.1093/logcom/4.3.217

H. Bachmair, C. Ganzinger, W. Lynch, and . Snyder, Basic paramodulation and superposition, Proceedings I1th International Conference on Aufomated Deduc- Saratoga Springs (N.1I, pp.462-476, 1992.
DOI : 10.1007/3-540-55602-8_185

T. Stickel and H. Zhang, Opening the AC-Unification Race, Journal of Automated Reasoning, pp.465-474, 1988.

S. [. Ballantyne and . Lankford, The Refutation Completeness of Blocked Permutative Narrowing and Resolution, Proceedings 4th Workshop on Automaied Deduction, 1979.

. Bibliographie, Associative Path Orderings, Proceedings lst Conference on Rewriting Techniques and Applications, 1985.

]. L. Bp85b, D. A. Bachmair, and . Plaisted, Termination Orderings For Associative-Commutative Rewriting Systems, Journal of Symbolic Computation, vol.1, pp.329-349, 1985.

G. [. Baird, R. W. Peterson, and . Wilkerson, Complete sets of reductions modulo associativity, commutativity and identity, Proceedings ard Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), volume 355 of Lecture Notes in Computer Science, 1989.
DOI : 10.1007/3-540-51081-8_98

]. D. Bra75 and . Brand, Proving Theorems with the Modification Method, SIAM Journal of Computing, vol.4, pp.412-430, 1975.

]. B. Buc65 and . Buchberger, An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-dimensional Polynomial Ideal, p.1965

]. B. Buc79 and . Buchberger, A Criterion for Detecting Unnecessary Reductions in the Construction of Grobner Bases, Proceedings of EUROSAM'79, pp.3-21, 1979.

]. R. Bün91 and . Bündgen, Simulating Buchberger's Algorithm by Knuth-Bendix Completion, Proceedings 4th Conference on Rewriting Techniques and Applications, pp.386-397, 1991.

]. Bür91 and . Bürckert, A Resolution Principle for aLogie with Restricted Quantifiers, Lecture Notes in Artificial Intelligence, vol.568, 1991.

]. J. Cha94 and . Chabin, Unification Générale par Surréduction Ordonnée Contrainte et Surréduction Dirigée, Thèse de Doctorat d'Université, 1994.

]. H. Com90 and . Comon, Solving Symbolic Ordering Constraints, International Journal of Foundations of Computer Sciences, vol.1, issue.4, pp.387-411, 1990.

N. [. Caferra and . Zabel, A method for simultaneous search for refutations and models by equational constraint solving, Journal of Symbolic Computation, vol.13, issue.6, pp.613-641, 1992.
DOI : 10.1016/S0747-7171(10)80014-8

]. N. Der82 and . Dershowitz, Orderings for Term-Rewriting Systems, Theoretical Computer Science, vol.17, pp.279-301, 1982.

J. Dershowitz and . Jouannaud, Rewrite Systems, J. van Leeuwen, edit or, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

E. Domenjoud, Outils pour la déduction automatique dans les théories associativescommutatives, Thèse de Doctorat d'Université, 1991.

]. E. Dom92, =. Domenjoud, +. .. Ac-pyl, and . Pyq, A Technical Note on AC-Unification. The Number of Minimal Unifiers of the Equation O:Xl + ... + o:x p, Journal of A utomated Reasoning, vol.8, pp.39-44, 1992.

S. Eker, Sorne ideas on elementary matching. note technique, 1993.

. Fortenbacher, Effizienles Rechnen in AC-Gleichungstheorien, 1989.

G. Gottlob and A. Leitsch, On the efficiency of subsumption algorithms, Journal of the ACM, vol.32, issue.2, pp.280-295, 1985.
DOI : 10.1145/3149.214118

P. Gnaedig and . Lescanne, Proving termination of associative commutative rewriting systems by rewriting, Proceedings 8th International Conference on Automated Deduction, pp.52-61, 1986.
DOI : 10.1007/3-540-16780-3_79

. Gnaedig, Preuves de terminaison des systèmes de réécriture associatifs-commutatifs: une méthode fondée sur la réécriture elle-même, Thèse de Doctorat de Troisième Cycle, 1986.

M. Haberstrau, About the Completeness of Strict Superposition, 1990.

J. Herbrand, Recherches sur la Théorie de la Démonstration, 1930.

J. Hsiang and M. Rusinowitch, On word problems in equational theories, Ottmann Proceedings of Lf.th International Colloquium on Automata, Languages and Programming, pp.54-71, 1987.
DOI : 10.1007/3-540-18088-5_6

URL : https://hal.archives-ouvertes.fr/inria-00075875

J. Hsiang and M. Rusinowitch, Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method, Journal of the ACM, vol.38, issue.3, pp.559-587, 1991.
DOI : 10.1145/116825.116833

]. G. Bibliographie-[-hue72 and . Huet, Constrained Resolution: A Complete Method for Higher Order Logic, 1972.

[. Jouannaud and H. Kirchner, Completion of a Set of Rules Modulo a Set of Equations, Preliminary version in Proceedings llth ACM Symposium on Prindples of Programming Languages, pp.1155-1194, 1984.
DOI : 10.1137/0215084

[. Jouannaud and C. Kirchner, Solving Equations in Abstract Algebras: a Rulebased Survey of Unification, Computational Logic. Essays in honor of Alan Robinson, pp.257-321, 1991.

J. (. Jaffar and . Lassez, Constraint logic programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '87, pp.111-119, 1987.
DOI : 10.1145/41625.41635

[. Jouannaud and C. Marché, Completion modulo associativity, commutativity and identity (AC1), Proceedings of DISCO'90, pp.111-120, 1990.
DOI : 10.1007/3-540-52531-9_130

]. Jouannaud and M. Okada, Satisnability of Systems of Ordinal Notations wïth the Subterm Property Is Deddable, Proceedings 18th ICALP Conference, 1991.

]. H. Kir85 and . Kirchner, Preuves par complétion dans les variétés d'algèbres, Thèse de Doctorat d'Etat, 1985.

H. [. Kirchner and . Kirchner, Constrained equational reasoning, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation , ISSAC '89, pp.382-389, 1989.
DOI : 10.1145/74540.74585

H. [. Kirchner, M. Kirchner, and . Rusinowitch, Deduction with Symbolic Constraints, pp.9-52, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00077103

D. [. Kapur, P. Musser, and . Narendran, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Journal of Symbolic Computation, vol.6, issue.1, 1985.
DOI : 10.1016/S0747-7171(88)80019-1

P. [. Kapur and . Narendran, Double-exponential complexity of computing a complete set of AC-unifiers, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, 1992.
DOI : 10.1109/LICS.1992.185515

]. D. Koz91 and . Kozen, A Completeness Theorem for Kleene Algebras and the Algebra Regular Events, Proceedings 6th IEEE Symposium on Logic in Computer Science, pp.214-225, 1991.

R. [. Kounalis, On word problems in Horn theories, Proceedings lat International Workshop on Conditional Term Rewriting Systems See also the extended version published in Journal of Symbolic Computation Ringeissen. Constraint Solving by Narrowing in Combined Algebraie Domains Proceedingsl1th International Conference on Logic Progmmming, pp.144-160, 1987.
DOI : 10.1007/3-540-19242-5_12

]. M. Lai89 and . Lai, On How to Move Mountains 'Associatively and Commutatively, Proceedings Srd Conference on Rewriting Techniques and Applications , Chapel Hill (N.C., USA), pp.187-202, 1989.

]. D. Lan79 and . Lankford, On Proving Term Rewriting Systems are Noetherian, 1979.

]. D. Lb77a, A. Lankford, and . Ballantyne, Decision Procedures for Simple Equational Theories with Permutative Axioms: Complete Sets of Permutative Reductions, UnÎv. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.

]. D. Lb77b, A. Lankford, and . Ballantyne, Decision Procedures for Simple Equational Theories with Associative Commutative Axioms: Complete Sets of Associative Commutative Reductions, 1977.

. Leseanne, Implementation of Completion by Transition Rules + Control

W. Lusk, R. Mccune, S. Overbeek, L. Winker, and . Wos, Automated Reasoning Contributes to Mathematics and Logic, Proceedings 10th International Conference on Automated Deduction, pp.485-499, 1990.

]. D. Bibliograpilie-(-lov78 and . Loveland, Automatic Theorem Proving, 1978.

W. [. Lynch and . Snyder, Redundancy criteria for constrained completion, Proceedings 5th Conference on Rewriting Techniques and Applications, pp.2-16, 1993.
DOI : 10.1007/3-540-56868-9_2

]. C. Mar93 and . Marché, Réécriture modulo une théorie présentée par un système convergent et décidabilité du problème du

]. W. Mcc88 and . Mccune, Challenge Equality Problems Lattice Theory, Proceedings 9th International Conference on Automated Deduction , Argonne (Ill., USA)MN90] U. Martin and T. Nipkow. Ordered Rewriting and Confluence Proceedings lOth International Conference on A utomated Deduction, pp.704-709, 1988.

M. [. Narendran and . Rusinowitch, Any Ground Associative-Commutative Theory Has a Finite Canonical System, Proceedings 4th Conference on Rewriting Techniques and Applications, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075236

A. Nieuwenhuis and . Rubio, Basic superposition is complete
DOI : 10.1007/3-540-55253-7_22

N. , R. Nieuwenhuis, and A. Rubio, AC-Superposition with Constraints: no AC-unifiers, Proceedings l1th International Conference on Automated Deduction, pp.477-491, 1992.
DOI : 10.1007/3-540-58156-1_40

URL : http://www.lsi.upc.es/~roberto/papers/cade94.ps.gz

P. Nutt, G. Réty, and . Smolka, Basic Narrowing Unification, pp.517-540, 1990.

E. Paul, A General Refutational Completeness Result for an Inference Procedure Based on Associative-Commutative Unification, Journal Symbolic Computation, vol.14, issue.6, pp.577-618, 1992.

E. Paul and E. Tree, Unpublished paper (E-mail: etienne.paul@issy.enet.fr). 70 pages, 1994. G. Peterson. A Technique for Establishing Completeness Results in Theorem Proving with Equality, SIAM Journal of Computing, vol.12, issue.1, pp.82-100, 1983.

G. E. Peterson, Complete sets of reductions with constraints, Stiekel, edit or Proceedings lOth International Conference on Automaied Deduction, pp.381-395, 1990.
DOI : 10.1007/3-540-52885-7_101

U. Petermann, Building in Equational Theories into the Conneetion Method, Fundamental of Artificial Intelligence Research Lecture Notes Computer Science G. Plotkin. Building-in Equational Theories. Machine Intelligence, vol.535, issue.7, pp.156-16973, 1972.

J. Pais and G. E. Peterson, Using forcing to prove completeness of resolution and paramodulation, Journal of Symbolic Computation, vol.11, issue.1-2, pp.3-19, 1991.
DOI : 10.1016/S0747-7171(08)80130-7

G. E. Peterson and M. , Complete Sets of Reductions for Some Equational Theories, Journal of the ACM, vol.28, issue.2, pp.233-264, 1981.
DOI : 10.1145/322248.322251

. Ringeissen, Combinaison de Résolutions de Contraintes, 1993.

A. Rubio and R. Nieuwenhuis, A precedence-based total AC-compatible ordering
DOI : 10.1007/3-540-56868-9_28

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

A. Rubio, A utomated Deduction with Constrained Clauses, 1994.

. Iv1 and . Rusinowiteh, Démonstration automatique -Techniques de réécriture. InterEditions, 1989.

M. Rusinowiteh, Theorem-proving with resolution and superposition, Journal of Symbolic Computation, vol.11, issue.1-2, pp.21-49, 1991.
DOI : 10.1016/S0747-7171(08)80131-9

C. [. Snyder and . Lynch, Basic Paramodulation, Proceedings 5th International Workshop on Unification, 1991.

J. R. Slagle, Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM, vol.14, issue.4, pp.687-697, 1967.
DOI : 10.1145/321420.321428

. Slagle, Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Assodativity. Journal of the A CM, vol.21, issue.4, pp.622-642, 1974.
DOI : 10.1145/321850.321859

M. E. Stickel, A Unification Algorithm for Associative-Commutative Functions, Journal of the ACM, vol.28, issue.3, pp.423-434, 1981.
DOI : 10.1145/322261.322262

]. L. Vig93 and . Vigneron, Basic AC-Paramodulation, Proceedings of the 2nd CCL Workshop, 1993.

. Vig94b and . Vigneron, Superposition in Theories: Proof of Completeness by Semantic Trees, 1994.

]. U. Wer92 and . Wertz, First-Order Theorem Proving Modulo Equations, 1992.

]. F. Win84 and . Winkler, The Ch1trch-RO/~ser in Computer Algebm and rem Proving: an Investigation of Critical-pairsjCompletion Algorithms Zhang and Do Kapur. First-order Theorem Proving Using Conditional Rewrite Rules, Proceedings 9th International rence on Automated Deduction, Argonne (Ill., USA), pp.1-20, 1984.