Logique propositionnelle

17.1 Introduction et motivation

La logique propositionnelle manipule des formules construites sur des variables booléennes à l'aide des connecteurs non, et, ou. Savoir si une formule est satisfiable (rendue vraie par un choix de valeurs) est le problème SAT, central en informatique théorique et omniprésent en pratique (vérification, planification, circuits).

Ce chapitre est aussi une synthèse du cours : une formule se modélise par un type somme récursif (chapitre 3), s'évalue par récursion sur sa structure, et sa satisfiabilité se décide par retour sur trace sur les valuations (chapitre 11), à l'aide d'un tableau de booléens (chapitre 5). La logique propositionnelle est le terrain de jeu idéal de la programmation fonctionnelle.

17.2 Représenter une formule

Une formule est : une variable, la négation d'une formule, la conjonction (et) ou la disjonction (ou) de deux formules. C'est un type récursif, comme les arbres du chapitre 3 — d'ailleurs une formule est un arbre.

type formule =
  | Var of int                       (* variable numérotée *)
  | Non of formule
  | Et of formule * formule
  | Ou of formule * formule