**
Hélène
Kirchner and Pierre-Etienne
Moreau
Section: Computation
Level: Introductory
**

Rules are largely used in Computer Science, from the artificial intelligence community to logic, functional and constraint programming. Computation rules are aimed to compute as fast as possible a unique result, while deduction rules are controlled by strategies and are better suited for search.

This lecture first introduce the concept of rewriting which is behind rule-based systems. Rewriting is first presented as an abstract relation on terms, and properties of such relations, mainly confluence and well-foundedness, are introduced. Confluence is the key concept to ensure the determinism of a rewriting relation seen as a computation process. Well-foundedness ensures that any computation terminates.

Then the rewriting logic and the rewriting calculus are defined and shown to be especially suited to describing concurrent and non-deterministic computations.

The lecture also presents the ELAN system that provides an environment for specifying and prototyping in a language based on rewrite rules controlled by strategies. Some concepts and techniques behind the implentation of the system are presented: compilation of matching and reduction integrating associative and commutative functions, non deterministic computations returning several results and a strategy language to control rewriting.

Examples illustrate how ELAN supports the design of theorem provers, constraint solvers and decision procedures and offers a modular framework for studying their combination.

Basic notions of universal algebra (terms, substitutions), tree automata, first-order logic.

- reader
- slides:Rule-based computation and deduction
- slides: ELAN
- slides: Logic and calculus for rewriting
- slides: Compilation of ELAN
- slides: Applications and future developments

Hélène Kirchner

Pierre-Etienne Moreau

INRIA Lorraine & LORIA

Technopôle de Nancy Brabois - Campus Scientifique

615, rue du Jardin Botanique

BP-101

F-54602 Villers-lès-Nancy

FRANCE

Fax: 33 3 83 27 83 19

Phone: 33 3 83 59 30 12 or 33 3 83 59 30 54 (secretary)

Helene.Kirchner@loria.fr

Pierre-Etienne.Moreau@loria.fr

http://www.loria.fr/~hkirchne

http://www.loria.fr/~moreau