Kirchner and Pierre-Etienne
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.
INRIA Lorraine & LORIA
Technopôle de Nancy Brabois - Campus Scientifique
615, rue du Jardin Botanique
Fax: 33 3 83 27 83 19
Phone: 33 3 83 59 30 12 or 33 3 83 59 30 54 (secretary)