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:

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.)
Logique équationnelle et complétion, terminaison, etc., les 10 séances suivantes, par Evelyne Contejean et Xavier Urbain.
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:

(fin 2009) Un petit peu de réécriture, text and solution.
(fin 2008) Résolution équationnelle, à contraintes, text and solution.
(fin 2006) Simplification criteria, text and solution.
(fin 2005) Semantic resolution, text and solution.
(printemps 2004, cours de vérification de protocoles cryptographiques) Spi-calcul et classes H₁ et H₂, énoncé long et corrigé.
(printemps 2003, cours de vérification de protocoles cryptographiques) La classe H₁ de Nielson, Nielson et Seidl, énoncé long et corrigé.

Au passage, vous pourrez trouver plus d'informations sur les examens de 2003 et de 2004 dans mon papier Deciding H₁ by Resolution, et bien sûr dans le papier original.
(1999, cours de démonstration automatique du DEA Programmation) Sous-classes décidables de la logique du premier ordre, énoncé et corrigé.
(1997, cours de démonstration automatique du DEA Programmation) La méthode inverse (seule la partie I est pertinente ici), énoncé et corrigé.

This document was translated from L^AT_EX by H^EV^EA.

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

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