Back

Rule-based Computation and Deduction

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

Description

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.

Prerequisites

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

Materials

Lecturers

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