. [. @bullet and . @bullet, V(8)in?? 8] . v(1) in?, ? [0, ..? 8] . V(4) in? [O ?.. ,8] .nilll V(1»=?0&V(3»=?0&V(2)<=?8&V(4)<=?8&V(4)=?V(3) (+), p.2

J. M. Andreoli, U. M. Borghoff, S. Castellani, R. Pareschi, and G. Teege, Agent Based Decision Support for managing Print Tasks, Proceedings of the PAAM'9S, 1998.

J. Abrial, The B-Book: Assigning Programs ta Meanings, 1996.
DOI : 10.1017/CBO9780511624162

M. Abadi and L. Cardelli, A Theory of Objects, 1996.
DOI : 10.1007/978-1-4419-8598-9

P. Albert and F. Fages, XRETE: un outil pour les systèmes experts temps réel, Génie Logiciel fj Systèmes Experts, vol.28, pp.22-34, 1992.

K. Arnold and J. Gosling, The Java programming language, 1996.

M. Ayel and J. P. Laurent, Validation, Verification and Test of Knowledge-Based Systems, 1991.

C. Alvarado and Q. Nguyen, ELAN for equational reasoning in Coq, Proceeding of 2nd Workshop on Logical Prameworks and Metalanguages, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00107864

. Barringer, Up and Down The Temporal Way, The Computer Journal, vol.30, issue.2, 1985.
DOI : 10.1093/comjnl/30.2.134

E. Beffara, O. Bournez, H. Kacem, and C. Kirchner, Verification of timed automata using rewrite rules and strategies, technical report, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00100535

B. Cherifa and P. 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

B. G. Buchanan, E. A. Feigenbaum, and M. Dendral, Dendral and meta-dendral: Their applications dimension, Artificial Intelligence, vol.11, issue.1-2, pp.5-24, 1978.
DOI : 10.1016/0004-3702(78)90010-3

L. Brownston, R. Farrell, E. Kant, and N. Martin, Programming Expert Systems in OPS5: An Introduction ta Rule-based Programming, 1985.

E. Borger and J. Huggins, Abstract State Machines, Commented ASM Bibliography . Bulletin of EATCS, vol.64, pp.105-127, 1988.
DOI : 10.1007/978-3-642-18216-7

G. Birkhoff, On the Structure of Abstract Algebras, Mathematical Proceedings of the Cambridge Philosophical Society, vol.31, issue.04, pp.433-454, 1935.
DOI : 10.1017/S0305004100013463

P. Borovansky, C. Kirchner, and H. Kirchner, A functional view of rewriting and strategies for a semantics of ElAN, The Third Fuji International
URL : https://hal.archives-ouvertes.fr/inria-00098628

F. Baader and T. Nipkow, Term Rewriting and all that, 1998.

. Borovansky, Implementation of higher-order unification based on calculus of explicit substitution, Proceedings of the SOFSEM'95: Theory and Practice of Informatics, pp.363-368, 1995.
DOI : 10.1007/3-540-60609-2_18

P. Borovansky, Le contrôle de la réécriture: étude et implantation d'un formalisme de stratégies, 1998.

L. Bachmair and D. Plaisted, Associative path orderings, Proceedings lst Conference on Rewriting Techniques and Applications, 1985.
DOI : 10.1007/3-540-15976-2_11

. Brézillon, Successes and failures of KBSs in real-world aplications, Report on the International Conference. Knowledge-Based Systems, pp.253-257, 1998.

Y. Caseau, Rule-aided constraint resolution in Laure, Proceedings of the International Workshop on Processing Declarative K nowledge (PDK'91), pp.237-256, 1991.
DOI : 10.1007/BFb0013534

Y. Caseau, Constraint satisfaction with an object-oriented knowledge representation language, Applied Intelligence, vol.8, issue.2, pp.157-184, 1994.
DOI : 10.1007/3-540-55015-1_14

C. Castro, Building Constraint Satisfaction Problem Solvers Using Rewrite Rules and Strategies, Fundamenta Informaticae, vol.34, pp.263-293, 1998.

C. Castro, Une approche déductive de la résolution de problèmes de satisfaction de contraintes, 1998.

H. Cirstea, Le Rho Calcul: Fondements et Applications, 2000.

H. Cirstea and C. Kirchner, Theorem Proving Using Computational Systems: The Case of the B Predicate Prover, Workshop CCL '97, 1997.

H. Cirstea and C. Kirchner, Combining higher-order and first-order computation using p-calculus: Towards a semantics of ELAN, Frontiers of Combining Systems, pp.95-120, 1999.

H. Cirstea and C. Kirchner, An introduction to the rewriting calculus, 1999.

H. Cirstea and C. Kirchner, Specifying Authentication Protocols Using Rewriting and Strategies, Third International Workshop on Practical Aspects of Declarative Languages, 2001.
DOI : 10.1007/3-540-45241-9_10

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

H. Cirstea, C. Kirchner, and L. Liquori, Matching Power, 2000.
DOI : 10.1007/3-540-45127-7_8

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

H. Cirstea, C. Kirchner, and L. Liquori, Matching power The Netherlands, Lecture Notes in Computer Science, Proceedings 12th Conference on Rewriting Techniques and Applications, 2001.

H. Cirstea, C. Kirchner, and L. Liquori, The Rho Cube, Proceedings of FOSSACS'200l, 2001.
DOI : 10.1007/3-540-45315-6_11

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

Y. Caseau and F. Laburthe, CLAIRE: Combining objects and rules for problem solving, Proceedings of the JICSLP'96 workshop on multi-paradigm logic programming, 1996.

. Clavel, Reflection in generallogics, rewriting logic, and Maude, 1998.

M. Dauchet, Simulation of Turing machines by a left-linear rewrite rule, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), pp.109-120, 1989.
DOI : 10.1007/3-540-51081-8_103

M. Duribreux-cocquebert, C. Kolski, and B. Houriez, Towards an integration of cognitive ergonomies concepts in knowledge based system development methodologies, Proceedings 6th IFAC/IFIP/IFORS/IEA Symposium on Analysis, Design and Evaluation of Man-Machine Systems, M.I. T, 1995.

F. Durân, S. Eker, P. Lincoln, and J. Meseguer, Principles of Mobile Maude, Procs, pp.73-85, 2000.
DOI : 10.1007/978-3-540-45347-5_7

. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

. Dershowitz, Termination of rewriting, Journal of Symbolic Computation, vol.3, issue.1-2, pp.69-116, 1987.
DOI : 10.1016/S0747-7171(87)80022-6

G. Dowek, T. Hardin, and C. Kirchner, Higher Order Unification via Explicit Substitutions, Information and Computation, vol.157, issue.1-2, pp.183-235, 2000.
DOI : 10.1006/inco.1999.2837

URL : https://hal.archives-ouvertes.fr/hal-01199528

N. Dershowitz and J. Jouannaud, Rewriting systems, pp.243-320, 1990.

R. Davis and J. King, An overview of production systems, Machine Intelligence, vol.10, pp.300-332, 1977.
DOI : 10.21236/ADA019702

H. Dubois and H. Kirchner, Actions and Plans in ELAN, Proceedings of the Workshop on Strategies in Automated Deduction -CADE-15 Gramlich and F. Pfenning, pp.35-45, 1998.

H. Dubois and H. Kirchner, Modelling Planning Problems with Rules and Strategies, 1999.

H. Dubois and H. Kirchner, Objects, rules and strategies in ELAN, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00099054

H. Dubois and H. Kirchner, Objects, rules and strategies in ELAN, Proceedings of the second AMAST workshop on Algebraic Methods in Language Processing, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00099054

H. Dubois and H. Kirchner, Rule Based Programming with Constraints and Strategies, New Trends in Constmints, Papers /rom the Joint ERCIM/Compulog-Net Workshop, Cyprus, pp.274-297, 1999.
DOI : 10.1007/3-540-44654-0_14

G. Denker, J. Meseguer, and C. Talcott, FormaI Specification and Analysis of Active Networks and Communication Protocols: the Maude Experience, Proceedings DARPA Information Survivability Conference and Exposition DICEX 2000, pp.251-265, 2000.

N. Dershowitz and M. Okada, A rationale for conditional equational programming, Theoretical Computer Science, vol.75, issue.1-2, pp.111-138, 1990.
DOI : 10.1016/0304-3975(90)90064-O

J. Durkin, Expert Systems, Catalog of Applications. Intelligent Computer Systems Inc., PO Box 4117, pp.444321-117, 1993.

K. D. Eason, S. Harker, R. F. Raven, J. R. Brailsford, and A. D. Cross, Expert or assistant: Supporting power engineers in the management of electricity distribution, AI & Society, vol.11, issue.1, pp.91-104, 1995.
DOI : 10.1007/BF01174481

F. Fages and G. Huet, Complete sets of unifiers and matchers in equational theories, Theoretical Computer Science, vol.43, issue.1, pp.189-200, 1986.
DOI : 10.1016/0304-3975(86)90175-1

K. Fisher, F. Honsell, and J. C. Mitchell, A Lambda Calculus of Objects and Method Specializatio n, Nordic Journal of Computing, vol.1, issue.1, pp.3-37, 1994.

R. Filman, Personal communication in [Der87}, 1978.

. Fissore, Terminaison par induction, 2000.

K. Futatsugi and A. Nakagawa, An overview of CAFE specification environment -an algebraic approach for creating, verifying, and maintaining formaI specifications over networks, Proceedings of the lst IEEE Int. Conference on Formai Engineering Methods, 1997.

C. L. Forgy, OPS5 User's Manual, 1981.
DOI : 10.21236/ADA106558

T. Frühwirth, Constraint Solving with Constraint Handling Rules, Proceedings of l2th International Symposium on Languages for Intensional Programming (ISLIP99), 1999.

K. Futatsugi and T. Sawada, Cafe as an extensible specification environment, Proceedings of the Kunming International CASE Symposium, 1994.

T. Genet and I. Gnaedig, Termination proofs using gpo ordering constraints, Proceedings 22nd International Colloquium on Trees in Algebra and Programming, pp.249-260
DOI : 10.1007/BFb0030601

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

I. Gnaedig, H. Kirchner, and O. Fissore, Termination of Rewriting with Local Strategies, Proceedings of 4th International Workshop on Strategies in Automated Deduction, IJCAR'Ol, 2001.

J. A. Goguen, C. Kirchner, H. Kirchner, A. Mégrelis, J. Meseguer et al., An introduction to OBJ 3, Proceedings lst International Workshop on Conditional Term Rewriting Systems Also as internaI report CRIN, pp.258-263, 1987.
DOI : 10.1007/3-540-19242-5_22

J. A. Goguen, Some design principles and theory for OBJ-O, a language for expressing and executing algebraic specifications of programs, Proceedings of International Conference on Mathematical Studies of Information Processing IFIP Working Group 2.2, pp.429-475, 1978.

A. Goldberg and D. Rohson, Smalltalk-80: The Language and Its Implementation

J. Giarratano and G. Riley, Expert Systems: Princip les 8 Programming, PWS-KENT, 1989.

R. F. Gambie, G. Roman, W. Ball, and H. C. Cunningham, Applying FormaI Verification Methods to Rule-Based Programs, International Journal of Expert Systems, vol.7, issue.3, pp.303-339, 1994.

H. Groiss, A FormaI Semantic for mOPS5, Proceedings of the Seventh IEEE International Conference on Tools with Artificial Intelligence, 1995.

J. A. Goguen and J. Tardo, OBJ-O preliminary users manual, Semantics and Theory of Computation Report, vol.10, 1977.

Y. Gurevich, Algorithms in the World of Bounded Resources The Universal Turing Machine -A Half-Century Story, pp.407-416, 1988.

Y. Gurevich, Logic and the Challenge of Computer Science, Theoretical Computer Science, pp.1-57, 1988.

A. Ginsberg and K. Williamson, Inconsistency and Redundancy Checking for Quasi-First- Order-Logic Knowledge Bases, International Journal of Expert Systems, vol.6, issue.3, pp.321-340, 1993.

E. Hart and R. O. Duda, PROSPECT OR -A computer based consultation system for minerai exploration. (SRI) Tecbnical Note 155, sri, 1977.

G. Huet and D. S. Lankford, On the uniform halting problem for term rewriting systems, 1978.

F. Hayes-roth, Rule-based systems, Communications of the ACM, vol.28, issue.9, pp.921-932, 1985.
DOI : 10.1145/4284.4286

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Preliminary version in 18th Symposium on Foundations of Computer Science, pp.797-821, 1977.
DOI : 10.1145/322217.322230

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

J. Jouannaud, P. Lescanne, and F. Reinig, Recursive decomposition ordering, Formai Description of Programming Concepts 2, pp.331-348, 1982.

D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

C. Kirchner and H. Kirchner, Rewriting, solving, proving. A preliminary version of a book available at, 1999.

C. Kirchner, H. Kirchner, and J. Meseguer, Operational semantics of OBJ-3, Proceedings of 15th International Colloquium on Automata, Languages and Programming, pp.287-301, 1988.
DOI : 10.1007/3-540-19488-6_123

C. Kirchner, H. Kircbner, and M. Vittek, Implementing computational systems with constraints, Proceedings of the first Workshop on Principles and Practice of Constraint Programming, pp.166-175, 1993.

C. Kirchner, H. Kirchner, and M. Vittek, Designing constraint logie programming languages using computational systems, Principles and Practice of Constraint Programming, pp.131-158, 1995.

C. Kirchner, H. Kirchner, and M. Vittek, ELAN V 1.17 User Manual, Inria Lorraine & Crin, 1995.

S. Kamin and J. Lévy, Attempts for generalizing the recursive path ordering. Unpublished manuscript, 1980.

J. W. Klop, Term Rewriting Systems, Handbook of Logic in Computer Science, 1990.

C. Kirchner, C. Lynch, and C. Scharff, A fine-grained concurrent completion procedure
URL : https://hal.archives-ouvertes.fr/inria-00073707

H. Kirchner and P. Moreau, Prototyping completion with constraints using computational systems, Proceedings 6th Conference on Rewriting Techniques and Applications, pp.438-443, 1995.
DOI : 10.1007/3-540-59200-8_79

H. Kirchner and P. Moreau, A reflective extension of ELAN, Proceedings of the first international workshop on rewriting logic, 1996.
DOI : 10.1016/S1571-0661(04)00038-6

S. Kocabas, A review of learning, The Knowledge Engineering Review, vol.6, issue.03, pp.195-222, 1991.
DOI : 10.1017/S0269888900005804

C. Kirchner and C. Ringeissen, Rule-Based Constraint Programming, Fundamenta Informaticae, vol.34, issue.3, pp.225-262, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00098476

D. Kapur, G. Sivakumar, and H. Zhang, A new method for proving termination of AC-rewrite systems, Proceedings IOth Conf. on Foundations of Software Technology and Theoretical Computer Science, pp.133-148, 1990.
DOI : 10.1007/3-540-53487-3_40

A. Ca-los, Validating and Verifying Knowledge-Based Systems, 1991.

D. S. Lankford, Canonical algebraic simplifications, 1975.

D. S. Lankford, Sorne approaches to equality for computationallogic: A survey and assessment . Memo ATP-36, 1977.

R. K. Lindsay, B. G. Buchanan, E. A. Feigenbaum, and J. Lederberg, Applications of Artificial Intelligence for Organic Chemistry: The DENDRAL Project, 1980.

L. Goc, Ontological models as shared model to validate a knowledge-based system, Proceedings of the Twelth Workshop on K nowledge Acquisition, M odeling and M anagement, 1999.

B. Liu, J. Jaffar, and H. C. Yap, Constraint rule-based programming, 1999.

S. Lee and R. M. , 0 'Keefe. Subsumption Anomalies in Hybrid Knowledge Bases, International Journal of Expert Systems, vol.6, issue.3, pp.299-320, 1993.

J. Laffey, W. A. Perkins, and T. A. Nguyen, Reasoning About Fault Diagnosis with LES, IEEE Expert, vol.1, issue.1, pp.13-20, 1986.
DOI : 10.1109/MEX.1986.5006493

J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, vol.96, issue.1, pp.73-155, 1992.
DOI : 10.1016/0304-3975(92)90182-F

B. Meyer, Eiffel: The Language, 1992.

A. Majchrzak and L. Gasser, On using artificial intelligence to integrate the design of organizational and process change in US manufacturing, AI & Society, vol.1, issue.4, pp.321-338, 1991.
DOI : 10.1007/BF02077438

P. Moreau and H. Kirchner, Compilation Techniques for Associative-Commutative Normalisation Second International Workshop on the Theory and Practice of Algebraic Specifications, Electronic Workshops in Computing, eWiC web site, 1997.

P. Moreau and H. Kirchner, A compiler for rewrite programs in associative-commutative theoriesFrinciples of Declarative Programming, number 1490 in Lecture Notes in Computer Science, pp.230-249, 1998.

J. Martl-oiiet and . Meseguer, Rewriting logic as a logical and semantical framework, 1993.

E. Monfroy, Collaboration de solveurs pour la programmation logique à contraintes, 1996.
URL : https://hal.archives-ouvertes.fr/tel-01747888

E. Monfroy, The Constraint Solver Collaboration Language of BALI, Frontiers of Combining Systems 2, Research Studies, pp.211-230, 1999.

P. Moreau, C. , and M. Vittek, A Pattern-Matching Compiler, Didier Parigot and Mark van den Brand Proceedings of the lst International Workshop on Language Descriptions, Toois and Applications
DOI : 10.1016/S1571-0661(04)80926-5

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

M. H. Newman, On theories with a combinalorial definition of equivalence, Annals of Math, pp.223-243, 1942.

A. Nguyen, Verifying Consistency of Production Systems, Proceedings of the third Conference on Artificial Intelligence Applications, 1987.

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079

T. A. Nguyen, W. A. Perkins, T. J. Laffey, and D. Pecora, Knowledge Base Verification, pp.69-75, 1987.
URL : https://hal.archives-ouvertes.fr/tel-01175929

D. Plaisted, A recursively defined ordering for proving termination of term rewriting sytems, Dept. of Computer Science Report, pp.78-943, 1978.

C. Llingeissen, Cooperation of decision procedures for the satisfiability problem, Proc. of FroCoS'96, pp.121-140, 1996.

C. Ringeissen, Prototyping combination of unification algorithms with the ELAN rule-based programming language, Proceedings 8th Conference on Rewriting Techniques and Applications, pp.323-326, 1997.
DOI : 10.1007/3-540-62950-5_81

B. K. Rosen, Tree-Manipulating Systems and Church-Rosser Theorems, Journal of the ACM, vol.20, issue.1, pp.160-187, 1973.
DOI : 10.1145/321738.321750

M. Rousset, On the consistency of knowledge bases: the COVADIS system, Proceedings of the 8th European Conference on Artificial Intelligence, pp.79-84, 1988.
DOI : 10.1016/0004-3702(86)90080-9

R. A. Stachowitz and J. B. Combs, Validation of Expert Systems, The Proceedings of the 20th Hawaii International Conference on System Sciences (HICSS), pp.689-695, 1987.

E. H. Shortliffe, Computer-Based Medical Consultations: MYCIN. Elsevier jNorth-Holland, 1976.

H. Simonis, Application development with the CHIP system, Constmint Databases and Applications, pp.1-21, 1995.
DOI : 10.1007/3-540-60794-3_11

L. A. Stein, H. Lieberman, and D. Ungar, Object-oriented concepts, applications, and databases , chapter A shared view of sharings: The treaty of Orlando, pp.31-48, 1989.

G. Smolka, The Oz Programming Model, Lecture Notes in Computer Science, vol.1000, pp.324-343, 1995.
DOI : 10.1007/BFb0015252

J. G. Schmolze and W. Snyder, Using Confluence to Control Parallei Production Systems, Second International Workshop on Paralle! Processing for Artificial Intelligence

J. G. Schmolze and W. Snyder, A Tooi for Testing Confluence of Production Rule Systems

W. Snyder and J. G. Schmolze, Rewrite semantics for production rule systems: Theory and applications, Proceedings 13th International Conference on A vtomated Deduction, pp.508-522, 1996.
DOI : 10.1007/3-540-61511-3_110

W. Snyder and J. G. Schmolze, Detecting Redundant Production Rules, AAAI-97