Thèse présentée par
pour obtenir le titre de
DOCTEUR de L’UNIVERSITÉ D’ÉVRY VAL D’ESSONNE
Spécialité :
Date de soutenance : lundi 9 juillet 2007
Composition du jury
Yves
Régine
Marc
Agnès
Serena
Pascale
Thèse préparée au Laboratoire Informatique, Biologie Intégrative et Systèmes
Complexes (IBISC) de l’Université d’Évry Val d’Essonne - FRE 2873 du CNRS.Introduction 7
I Préliminaires : fondements théoriques 11
1 Formalismes de spécifications 13
1.1 La logique des prédicats du premier ordre . . . . . . . . . . . . .
1.1.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.1.2 Sémantique . . . . . . . . . . . . . . . . . . . . . . . . .
1.2 Les systèmes de preuve . . . . . . . . . . . . . . . . . . . . . . .
1.2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . .
1.2.2 Les systèmes formels . . . . . . . . . . . . . . . . . . . .
1.2.3 Le calcul des séquents . . . . . . . . . . . . . . . . . . .
1.3 La logique équationnelle . . . . . . . . . . . . . . . . . . . . . .
1.3.1 Présentation . . . . . . . . . . . . . . . . . . . . . . . . .
1.3.2 Formules équationnelles simplifiées . . . . . . . . . . . .
1.4 Les spécifications algébriques . . . . . . . . . . . . . . . . . . .
1.4.1 Préliminaires . . . . . . . . . . . . . . . . . . . . . . . .
1.4.2 Conséquences sémantiques . . . . . . . . . . . . . . . . .
1.4.3 Autre exemple : les piles . . . . . . . . . . . . . . . . . .
2 Réécriture ...