Logique pour l'informatique

Cet ouvrage debute par une introduction a la logique des predicats du premier
ordre : syntaxe, semantique et preuves formelles. Il guide ensuite le lecteur
vers quelques uns de ses aspects plus avances : theoreme de completude,
theoreme d'indecidabilite. Se tournant ensuite vers les rapports de la logique
et de l'informatique, il presente les methodes algorithmiques de demonstration
automatique comme la resolution et l'unification ainsi que des applications
plus directes des concepts logiques au domaine informatique (probleme SAT,
bases de donnees relationnelles, verification de modele, etc.)

Sa lecture ne demande aucun prerequis en la matiere et peut s'adresser a tout
etudiant debutant en logique (licence ou master d'informatique, eleve
ingenieur). L'expose des notions de base de logique sont accompagnees de
nombreux exercices corriges.