**
François
Fages
Section: Logic and Computation
Level: Introductory
**

The purpose of this course is to introduce the semantics of Constraint Logic Programming (CLP) languages in First-Order logic and the subsequent methods for reasoning about CLP programs.

- Computation and Logic: the paradigm
of logic programming
- programs=theories, computation=proof search
- From Gödel's completeness theorem to the procedural interpretation of logic programs
- Constraint languages and Gödel's incompleteness theorem
- The class of Constraint Logic Programming languages CLP(X)

- Examples and demonstrations of CLP(X) programs
- CLP(H)-Prolog: deductive databases, list processing, meta-interpreters, theorem proving
- CLP(lambda): higher-order theorem proving
- CLP(R): linear programming and hybrid system modeling.
- CLP(FD): constraint propagation algorithms and combinatorial search problems.

- Formal semantics of CLP(X) languages
- Why? Observable properties and equivalences of programs
- The programming language versus theorem prover points of view
- Full abstraction theorems between operational and fixed point semantics
- Program analysis by abstract interpretation
- Completeness theorems w.r.t. the logical semantics.

- Lecture notes
- Slides 1: Introduction and Logical Background
- Slides 2: Operational Semantics of CLP Languages and Examples
- Slides 3: Fixpoint and Logical Semantics

Dr.Hab. François Fages

Projet Contraintes

INRIA Rocquencourt

BP 105

F-78153 Le Chesnay Cedex

France

http://contraintes.inria.fr/~fages

Francois.Fages@inria.fr

tel. (33) 1 39 63 57 09