Logique propositionnelle classique
Jean Goubault-Larrecq
Une logique est une syntaxe (une façon de construire l'ensemble
des formules), une sémantique (une description de ce que ces
formules signifient), et un système de preuve (qui nous permet de
calculer la signification des formules en construisant des preuves).
Nous exposons la syntaxe, la sémantique et quelques systèmes de
preuve pour la logique propositionnelle classique, une des logiques
les plus simples, mais aussi les moins expressives. Ceci nous
mènera à des méthodes de démonstration automatique pour cette
logique: tableaux, résolution propositionnelle, méthode de
Davis-Putnam-Logemann-Loveland method, et diagrammes de décision
binaire (BDD). Nous terminons ce chapitre par quelques digressions,
que le lecteur pourra sauter en première lecture.
This document was translated from LATEX by HEVEA.
This document was cut into pieces by
HACHA.