Cours 2.5 du MPRI “démonstration automatique”

Jean Goubault-Larrecq
LSV/UMR 8643, CNRS, ENS Cachan & INRIA Futurs projet SECSI
61 avenue du président-Wilson, F-94235 Cachan Cedex
goubault@lsv.ens-cachan.fr
Phone: +33-1 47 40 75 68   Fax: +33-1 47 40 75 21


    Cours
Où? Where? Chevaleret,
    salle 0D1.
Quand? When? Le mardi de 16h15 à 18h45
Par qui? Who? Jean Goubault-Larrecq
    Evelyne Contejean
    Xavier Urbain
    Ralf Treinen

Le cours est découpé en quatre parties / The lectures are split in four parts:
  1. Résolution et raffinements, stratégies d'élimination de redondances, classes décidables de la logique du premier ordre, les 5 premières séances, par Jean Goubault-Larrecq.

    (Resolution and refinements, redundancy elimination strategies, decidable classes of first-order logic, first 4 sessions.)
  2. Logique équationnelle et complétion, terminaison, etc., les 10 séances suivantes, par Evelyne Contejean et Xavier Urbain.
  3. Ralf Treinen, contraintes, théories concrètes (arithmétique de Presburger, MSO, etc.), automates.

    (Constraints, concrete theories—Presburger arithmetic, MSO, etc.—, automata.)
Le poly est en français, et couvre la première partie; an English version is also available, which covers roughly the same themes, including added bonuses on paramodulation theorem proving.

Devoir à la maison / Homework assignment: text. À rendre le mardi 26 octobre (à Xavier Urbain ou à Evelyne Contejean; ou à moi, par courrier, ou en format éléctronique, voir ma page Web). En français, or in English, as you prefer.

Bon, il faut que je stop now, mixing English and français commence à me taper on the nerves.

Quelques sujets d'examens sur des sujets connexes que j'ai posés dans le temps / Some exam questions on related topics that I asked in more or less ancient times:
This document was translated from LATEX by HEVEA.