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) ,
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 ,
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 ,
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 ,
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~ ,
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 ,
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
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
Completion for Rewriting Modulo a Congruence, Theoretical Computer Science, vol.67, issue.2-3, pp.173-202, 1989. ,
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
Associative-commutative superposition, 1993. ,
DOI : 10.1007/3-540-60381-6_1
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
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
Opening the AC-Unification Race, Journal of Automated Reasoning, pp.465-474, 1988. ,
The Refutation Completeness of Blocked Permutative Narrowing and Resolution, Proceedings 4th Workshop on Automaied Deduction, 1979. ,
Associative Path Orderings, Proceedings lst Conference on Rewriting Techniques and Applications, 1985. ,
Termination Orderings For Associative-Commutative Rewriting Systems, Journal of Symbolic Computation, vol.1, pp.329-349, 1985. ,
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
Proving Theorems with the Modification Method, SIAM Journal of Computing, vol.4, pp.412-430, 1975. ,
An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-dimensional Polynomial Ideal, p.1965 ,
A Criterion for Detecting Unnecessary Reductions in the Construction of Grobner Bases, Proceedings of EUROSAM'79, pp.3-21, 1979. ,
Simulating Buchberger's Algorithm by Knuth-Bendix Completion, Proceedings 4th Conference on Rewriting Techniques and Applications, pp.386-397, 1991. ,
A Resolution Principle for aLogie with Restricted Quantifiers, Lecture Notes in Artificial Intelligence, vol.568, 1991. ,
Unification Générale par Surréduction Ordonnée Contrainte et Surréduction Dirigée, Thèse de Doctorat d'Université, 1994. ,
Solving Symbolic Ordering Constraints, International Journal of Foundations of Computer Sciences, vol.1, issue.4, pp.387-411, 1990. ,
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
Orderings for Term-Rewriting Systems, Theoretical Computer Science, vol.17, pp.279-301, 1982. ,
Rewrite Systems, J. van Leeuwen, edit or, 1990. ,
DOI : 10.1016/B978-0-444-88074-1.50011-1
Outils pour la déduction automatique dans les théories associativescommutatives, Thèse de Doctorat d'Université, 1991. ,
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. ,
Sorne ideas on elementary matching. note technique, 1993. ,
Effizienles Rechnen in AC-Gleichungstheorien, 1989. ,
On the efficiency of subsumption algorithms, Journal of the ACM, vol.32, issue.2, pp.280-295, 1985. ,
DOI : 10.1145/3149.214118
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
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. ,
About the Completeness of Strict Superposition, 1990. ,
Recherches sur la Théorie de la Démonstration, 1930. ,
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
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
Constrained Resolution: A Complete Method for Higher Order Logic, 1972. ,
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
Solving Equations in Abstract Algebras: a Rulebased Survey of Unification, Computational Logic. Essays in honor of Alan Robinson, pp.257-321, 1991. ,
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
Completion modulo associativity, commutativity and identity (AC1), Proceedings of DISCO'90, pp.111-120, 1990. ,
DOI : 10.1007/3-540-52531-9_130
Satisnability of Systems of Ordinal Notations wïth the Subterm Property Is Deddable, Proceedings 18th ICALP Conference, 1991. ,
Preuves par complétion dans les variétés d'algèbres, Thèse de Doctorat d'Etat, 1985. ,
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
Deduction with Symbolic Constraints, pp.9-52, 1990. ,
URL : https://hal.archives-ouvertes.fr/inria-00077103
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
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
A Completeness Theorem for Kleene Algebras and the Algebra Regular Events, Proceedings 6th IEEE Symposium on Logic in Computer Science, pp.214-225, 1991. ,
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
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. ,
On Proving Term Rewriting Systems are Noetherian, 1979. ,
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. ,
Decision Procedures for Simple Equational Theories with Associative Commutative Axioms: Complete Sets of Associative Commutative Reductions, 1977. ,
Implementation of Completion by Transition Rules + Control ,
Automated Reasoning Contributes to Mathematics and Logic, Proceedings 10th International Conference on Automated Deduction, pp.485-499, 1990. ,
Automatic Theorem Proving, 1978. ,
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
Réécriture modulo une théorie présentée par un système convergent et décidabilité du problème du ,
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. ,
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
Basic superposition is complete ,
DOI : 10.1007/3-540-55253-7_22
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
Basic Narrowing Unification, pp.517-540, 1990. ,
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. ,
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. ,
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
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. ,
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
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
Combinaison de Résolutions de Contraintes, 1993. ,
A precedence-based total AC-compatible ordering ,
DOI : 10.1007/3-540-56868-9_28
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 utomated Deduction with Constrained Clauses, 1994. ,
Démonstration automatique -Techniques de réécriture. InterEditions, 1989. ,
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
Basic Paramodulation, Proceedings 5th International Workshop on Unification, 1991. ,
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
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
A Unification Algorithm for Associative-Commutative Functions, Journal of the ACM, vol.28, issue.3, pp.423-434, 1981. ,
DOI : 10.1145/322261.322262
Basic AC-Paramodulation, Proceedings of the 2nd CCL Workshop, 1993. ,
Superposition in Theories: Proof of Completeness by Semantic Trees, 1994. ,
First-Order Theorem Proving Modulo Equations, 1992. ,
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. ,