cours-tlpo

Les termes en logique et en programmationVersion préliminaireHubert Comon et Jean-Pierre JouannaudLaboratoire de Recherche en InformatiqueBât. 490CNRS et Université de Paris Sud91405 Orsay, Franceemail : comon,jouannau@lri.lri.frhttp ://www.lri.fr/ jouannau/biblio.html10 décembre 2003Table des matières1 Introduction 52 Algèbres de Termes 72.1 Termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.1.1 Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.1.2 Positions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.1.3 Termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82.1.4 Sous-termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102.1.5 Remplacement de sous-termes . . . . . . . . . . . . . . . . . . . . 112.1.6 Généralisations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112.2 -algèbres . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122.3 Homomorphismes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132.3.1 Substitutions et subsumption . . . . . . . . . . . . . . . . . . . . . 142.4 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 Logique équationnelle 173.1 Sémantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173.2 Problèmes du mot, d’unification, inductifs . . . . . . . . . . . . . . . . . . 173.3 Raisonnement équationnel . . . . . ...