Calcul propositionnel
E.S.I (2022-2023)
Module : RCR
Section : 2SID
Cours 1 : Calcul propositionnel
Le calcul des propositions est la première étape dans la définition de la logique et du raisonnement.
Il définit les règles de déduction qui relient les phrases entre elles, sans en examiner le contenu ; il est
ainsi une première étape dans la construction du calcul des prédicats, qui lui s’intéresse au contenu des
propositions.
Une logique comporte une syntaxe (pour définir les formules), une sémantique (pour définir le sens
des formules), et un système formel (pour prouver les formules).
1 Syntaxe
Dans la littérature logique, un symbole propositionnel est synonyme à variable propositionnel,
proposition atomique, formule atomique ou atome.
Le langage du calcul propositionnel est formé de :
— Symboles propositionnels : lettres de l’alphabet (P1 , P2 , ..., Q1 , Q2 , ...)
— Connecteurs logiques : ∨, ∧, ⇒, ⇔, ¬.
— Symboles auxiliaires : parenthèses.
Définition 1 L’ensemble Fp des formules du calcul propositionnel est définit comme suit :
— Tout symbole propositionnel est une formule ;
— Si ψ est une formule alors ¬ψ est une formule ;
— Si ψ et χ sont des formules, alors ψ ∨ χ, ψ ∧ χ, ψ ⇒ χ et ψ ⇔ χ sont des formules.
Exemple 1 .
1. P ∨ Q ⇒ ¬R ⇒ ⊥ et ((¬P ∨ Q) ∧ ¬P ) ∨ P sont des formules du calcul propositionnel.
2. ¬(⇒ P ), P (x) ⇔ Q(x) et R(x, y) ne sont pas des formules du calcul propositionnel.
Définition 2 L’ensemble SF p des sous formules d’une formule est défini comme suit :
— SF p (P ) = {P } ;
— SF p (¬ψ) = {¬ψ} ∪ SF p (ψ) ;
— SF p (ψ ∗ χ) = {ψ ∗ χ} ∪ SF p (ψ) ∪ SF p (χ), tel que ∗ représente l’un des connecteurs logiques :
∨, ∧, ⇒, ⇔.
Exercice 1 Considérez les formules du calcul propositionnel suivantes :
ψ1 := p ∧ (r ∧ ((¬q) ⇒ ¬p))
ψ2 := ((q ∨ ¬p) ⇒ (¬¬q ∨ ¬p)) ∧ ((¬¬q ∨ ¬p) ⇒ (¬p ∨ q))
Pour chaque formule ψi ∈ {ψ1 , ψ2 } :
1. Dessinez son arbre syntaxique.
2. Enumérez ses sous-formules.
2 Sémantique
L’évaluation d’une formule consiste à attribuer une valeur de vérité à ses propositions atomiques. En
admettant qu’une valuation est une application qui attribue à chaque variable propositionnelle une valeur
de vérité dans {0, 1}, alors la valeur 0 désigne le "faux" et la valeur 1 désigne le "vrai".
R.BOUSSAHA page 1
2.1 Modèle d’une formule Calcul propositionnel
Définition 3 la valuation d’une formule se détermine par extension de la valuation v aux sous-
formules de la façon suivante :
— v(¬ψ) = 1 − v(ψ)
— v(ψ ∨ χ) = max(v(ψ), v(χ))
— v(ψ ∧ χ) = min(v(ψ), v(χ))
— v(ψ ⇒ χ) = v(¬ψ ∨ χ)
2.1 Modèle d’une formule
Définition 4 Un modèle d’une formule ψ est une valuation v telle que v(ψ) = 1. On note mod(ψ)
l’ensemble des modèles de ψ.
Définition 5 — Une formule ψ est satisfaisable, consistante, ou cohérente si elle admet
au moins un modèle (i.e., il existe une valuation v telle que v(ψ) = 1).
— Une formule ψ est insatisfaisable, inconsistante, ou incohérente si elle n’admet aucun
modèle (i.e., si pour toute valuation v, v(ψ) = 0).
— Une formule ψ est valide ou une tautologie si v(ψ) = 1 pour toute valuation v . On note
|= ψ pour dire que ψ est une tautologie.
Exercice 2 1. Quelles sont les valuations qui donnent les mêmes valeurs de vérité à p ∧ q et p ⇒ q ?
2. Donnez les modèles de la formules p ∧ q ⇔ p ⇒ q
3. Est-ce que cette formule est (in)satisfaisable, valide ?
La proposition suivante explicite les liens existants entre la logique et l’algèbre ensembliste.
Proposition 1 Soient ψ et χ deux formules. En supposant que V al est l’ensemble de toutes les
valuations possibles d’une formule donnée, on a :
1. mod(¬ψ) = V al − mod(ψ)
2. mod(ψ ∨ χ) = mod(ψ) ∪ mod(χ)
3. mod(ψ ∧ χ) = mod(ψ) ∩ mod(χ)
4. |= ψ ⇒ χ ssi mod(ψ) ⊆ mod(χ)
Preuve. Exercice
Définition 6 Une formule χ est conséquence logique d’une formule ψ, et on note ψ |= χ, si
mod(ψ) ⊆ mod(χ).
Proposition 2 Soient ψ et χ deux formules propositionnelles.
1. ψ |= χ ssi |= ψ ⇒ χ
2. ψ ≡ χ ssi |= ψ ⇔ χ
Preuve. Exercice
2.2 Conséquence logique d’un ensemble de formules
On considère des ensembles de formules propositionnelles pour modéliser des problèmes de satisfaction de
contraintes. Une valuation satisfaisant toute formule de l’ensemble pourra donc se considérer comme une
solution du problème.
R.BOUSSAHA page 2
2.3 Décidabilité du calcul propositionnel Calcul propositionnel
Définition 7 Etant donné Γ un ensemble de formules, on définit le modèle de Γ comme une va-
luation v qui vérifie v(ψ) = 1 pout tout ψ ∈ Γ. On note mod(Γ) l’ensemble des modèles de Γ.
Définition 8 Un ensemble de formules Γ est satisfaisable s’il admet au moins un modèle
(i.e., mod(Γ) ̸= ∅). Il est insatisfaisable s’il n’admet aucun modèle (i.e., mod(Γ) = ∅), et on
note Γ |= ⊥.
Définition 9 Une formule ψ est conséquence logique de Γ si, et seulement si, toute valuation qui
donne 1 à toutes les formules de Γ donne 1 à ψ (i.e., mod(Γ) ⊆ mod(ψ)), on note Γ |= ψ
Exercice 3 On considère l’ensemble des formules propositionnelles Γ = {p ∨ q ∨ r, p ⇒ q, q ⇒ r}.
1. Trouver les modèles de Γ.
2. Les formules q ⇒ p, r sont-elles des conséquences logiques de Γ ?
2.2.1 Compacité
Le théorème de compacité sert à caractériser la conséquence logique dans les cas où l’ensemble des formules
est infini en ne considérant que des sous-ensembles finis.
Théorème 1 (Compacité) Un ensemble de formules propositionnelles Γ est satisfaisable si, et
seulement si, tout sous-ensemble fini de Γ est satisfaisable.
Par contraposée, le théorème de compacité peut s’énoncer de la façon suivante :
Théorème 2 (Compacité) Un ensemble de formules propositionnelles Γ est contradictoire si, et
seulement si, il existe un sous-ensemble fini de Γ contradictoire.
Preuve. A admettre.
Corollaire du théorème de compacité :
Corollaire 1 Une formule φ est conséquence d’un ensemble de formules Γ si, et seulement si, il
existe un sous-ensemble fini Γf ini de Γ tel que Γf ini |= φ.
Preuve. Exercice.
2.3 Décidabilité du calcul propositionnel
Une logique est décidable s’il existe un algorithme qui permet de déterminer pour chaque formule si elle
est valide ou pas.
Le calcul propositionnel est décidable. En effet, il suffit de tracer la table de vérité, et considérer tous les
cas possibles des variables propositionnelles pour savoir si une formule donnée est valide, satisfaisable ou
contradictoire. Mais la complexité de ce type d’algorithme est O(2n ), avec n le nombre des symboles propo-
sitionnels. Il y a plusieurs variantes de ces algorithmes, mais ils ont tous un coût exponentiel. Pour vérifier
la satisfaisabilité ou la validité de formules, ces algorithmes commencent par une étape de normalisation,
où on modifie la syntaxe tout en préservant la sémantique.
R.BOUSSAHA page 3
2.4 Equivalence entre formules Calcul propositionnel
2.4 Equivalence entre formules
Le principe de substitution est défini comme suit :
Définition 10 Soient ψ, χ, χ′ trois formules du calcul propositionnel,
— Si χ n’est pas une sous-formule de ψ, alors ψ[χ ← χ′ ] = ψ
— Sinon si ψ = χ alors ψ[χ ← χ′ ] = χ′
— Sinon
— Si ψ = ¬ψ ′ alors ψ[χ ← χ′ ] = ¬ψ ′ [χ ← χ′ ]
— Si ψ = ψ1 ∗ ψ2 alors ψ[χ ← χ′ ] = ψ1 [χ ← χ′ ] ∗ ψ2 [χ ← χ′ ]. ∗ est l’un des connecteurs
logiques ∨, ∧, ⇒, ou ⇔.
Proposition 3 Soient ψ, χ and χ′ trois formules du calcul propositionnel. Si χ ≡ χ′ alors ψ =
ψ[χ ← χ′ ].
Preuve. Exercice
Définition 11 On dit que la formule ψ est équivalente à la formule χ si elles ont les mêmes modèles
(i.e., mod(ψ) = mod(χ)), et on note ψ ≡ χ.
Le tableau suivant présente quelques équivalences classiques qui permettent de faire des substitutions.
Table 1 – Equivalences classiques.
Propriété Conjonction Disjonction
Commutativité ψ∧χ≡χ∧ψ ψ∨χ≡χ∨ψ
Associativité ψ1 ∧ (ψ2 ∧ ψ3 ) (ψ1 ∨ ψ2 ) ∨ ψ3
Elément neutre T∧ψ ≡ ψ∧T ≡ ψ ⊥∨ψ ≡ ψ∨⊥≡ ψ
Distributivité ψ1 ∧ (ψ2 ∨ ψ3 ) ≡ (ψ1 ∧ ψ2 ) ∨ (ψ1 ∧ ψ3 ) ψ1 ∨ (ψ2 ∧ ψ3 ) ≡ (ψ1 ∨ ψ2 ) ∧ (ψ1 ∨ ψ3 )
(ψ2 ∨ ψ3 ) ∧ ψ1 ≡ (ψ2 ∧ ψ1 ) ∨ (ψ3 ∧ ψ1 ) (ψ2 ∧ ψ3 ) ∨ ψ1 ≡ (ψ2 ∨ ψ1 ) ∧ (ψ3 ∨ ψ1 )
Complément ψ ∧ ¬ψ ≡ ¬ψ ∧ ψ ≡ ⊥ ψ ∨ ¬ψ ≡ ¬ψ ∨ ψ ≡ T
Lois de De Morgan ¬(ψ ∧ χ) ≡ ¬ψ ∨ ¬χ ¬(ψ ∨ χ) ≡ ¬ψ ∧ ¬χ
Idempotence ψ∧ψ ≡ψ ψ∨ψ ≡ψ
Elément absorbant ψ∧⊥≡⊥∧ψ ≡⊥ ψ∨T≡T∨ψ ≡T
Involution ¬¬ψ ≡ ψ
Implication ψ ⇒ χ ≡ ¬ψ ∨ χ
Contraposition ψ ⇒ χ ≡ ¬χ ⇒ ¬ψ
Curryfication ψ1 ⇒ (ψ2 ⇒ ψ3 ) ≡ (ψ1 ∧ ψ2 ) ⇒ ψ3
2.5 Formes normales
Soient ψ1 , ψ2 , ...ψn des formules du calcul
Wn propositionnel. Nous utilisons les notations suivantes :
V n
i=1 ψ i = ψ1 ∧ ψ 2 ∧ ... ∧ ψn et i=1 ψi = ψ1 ∨ ψ2 ∨ ... ∨ ψn
R.BOUSSAHA page 4
2.6 Mise sous forme clausale, en préservant l’équivalence Calcul propositionnel
On
V0 suppose également
Wque :
0
ψ
i=1 i = T et i=1 i = ⊥
ψ
Définition 12 Un littéral est une proposition atomique ou la négation d’une proposition atomique
de la forme P ou ¬P , où P est un symbole propositionnel.
Wn
Définition 13 Une clause disjonctive est une disjonction
Vn de littéraux notée i=1 li , et une clause
conjonctive est une conjonction de littéraux notée i=1 li , où li (1 ≤ i ≤ n) sont des littéraux.
Définition 14 Une formule est dite sous forme normale conjonctiveV(FNC), ou sous forme clausale
m Wni
si elle peut s’écrire comme une conjonction de clauses disjonctives i=1 j=1 lij . Une formule est
dite sous forme normale
W m V ni disjonctive (FND) si elle peut s’écrire comme une disjonction de clauses
conjonctives i=1 j=1 lij , où lij sont des littéraux.
2.6 Mise sous forme clausale, en préservant l’équivalence
L’algorithme consiste en l’application des trois étapes suivantes :
1. Appliquer la substitution suivante (en remplaçant le membre gauche par le membre droit) pour
éliminer l’implication : φ ⇒ ψ ← ¬φ ∨ ψ
2. Appliquer les substitutions suivantes, pour pousser la négation vers les symboles propositionnels :
¬¬φ ← φ, ¬(φ ∧ ψ) ← ¬φ ∨ ¬ψ, ¬(φ ∨ ψ) ← ¬φ ∧ ¬ψ
3. Appliquer les substitutions suivantes, pour pousser la disjonction vers les littéraux :
φ ∨ (ψ1 ∧ ψ2 ) ← (φ ∨ ψ1 ) ∧ (φ ∨ ψ2 )
Exercice 4 Normaliser la formule suivante : ¬(p ∧ (q ⇒ (r ∨ s))) ∧ (p ∨ q)
3 Le problème SAT
Définition 15 Le problème SAT est le problème de décision qui consiste à déterminer si φ ∈ Fp
donnée en entrée admet, ou non, un modèle.
Il y a de nombreux algorithmes qui permettent de résoudre SAT, nous en présentons quelques-uns, en
supposant que la formule dont il faut décider la satisfaisabilité est déjà en forme normale conjonctive.
Nous commençons par présenter quelques calculs (simplifications et substitutions) à appliquer sur les
formules en FNC.
3.1 Simplifications
Avant de chercher les modèles d’une formule sous forme clausale, nous pouvons optimiser les calculs qui
suivront en appliquant les règles suivantes :
— Tiers exclus : Les clauses comportant deux littéraux opposés sont valides et peuvent donc être
supprimées.
— Fusion : On peut supprimer la répétition d’un littéral dans une même clause.
— Subsumption (inclusion) : Etant données deux clauses C et C ′ , on dit que C subsume C ′ si C
est incluse dans C ′ , c’est-à-dire, si tout littéral apparaissant dans C apparaît aussi dans C ′ . Dans
ce cas on simplifie l’ensemble des clauses en supprimant C ′ .
3.2 Substitutions
Soit φ une formule sous forme clausale, et C l’ensemble de ses clauses. Le calcul d’une formule équivalente
à φ[p ← ⊥], ou φ[p ← T] peut se faire via une procédure syntaxique sur l’ensemble C :
— C[p ← T] : est l’ensemble obtenu de C en supprimant toutes les clauses contenant p, et en supprimant
¬p de toutes les clauses contenant ¬p.
— C[p ← ⊥] : est l’ensemble obtenu de C en supprimant toutes les clauses contenant ¬p, et en suppri-
mant p de toutes les clauses contenant p.
R.BOUSSAHA page 5
3.3 Algorithme Quine Calcul propositionnel
3.3 Algorithme Quine
La méthode parcourt l’arbre de toutes les solutions (l’arbre dont les branches complètes sont les valua-
tions, appelé aussi arbre sémantique). Chaque fois qu’une valeur de vérité est affectée à une variable
propositionnelle, le calcul se fait récursivement avec C[p ← T] ou C[p ← ⊥].
Algorithme de Quine
Entrée : un ensemble de clauses C
Sortie : vrai si C est satisfaisable ou faux sinon
Appliquer les étapes de simplifications sur l’ensemble de clauses
Si C = ∅ retourner vrai
Si C contient la clause ⊥ retourner faux
Choisir le prochain symbole propositionnel à partir d’une clause
Si Quine(C[p ← ⊥]) = vrai retourner vrai
Sinon retourner Quine(C[p ← T])
3.4 Algorithme de Davis-Putnam-Logemann-Loveland
L’algorithme DPLL peut être vu comme un raffinement de la méthode de Quine. L’amélioration principale
se résume en :
— La réduction du branchement via la propagation des clauses unitaires.
— L’utilisation d’heuristiques pour accélérer le parcours des solutions.
Algorithme DPLL
Entrée : un ensemble de clauses C
Sortie : vrai si C est satisfaisable ou faux sinon
Appliquer les étapes de simplifications sur l’ensemble de clauses
Si C = ∅ retourner vrai
Si C contient la clause ⊥ retourner faux
Si C contient la clause unitaire l retourner DP LL(C[l ← T])
Choisir un littéral l depuis une clause et x, y ∈ {⊥, T}, x ̸= y (avec une heuristique)
Si DP LL(C[l ← x]) = vrai retourner vrai
Sinon retourner DP LL(C[l ← y])
Littéraux purs : Si une variable propositionnelle apparaît seulement sous forme positive ou seulement
sous forme négative alors ses littéraux sont dits purs. On choisit un littéral pur l parmi ceux qui apparaissent
dans le plus de clauses, et on prend l ← T.
4 Système formel
Un système formel (ou système de preuve) est un ensemble de règles qui permettent d’inférer de nouvelles
conclusions à partir des prémisses. Il est constitué de :
— Langage et formules de ce langage ;
— Axiomes, qui sont des formules supposées être toujours vraies ;
— Règles d’inférence. Une règle d’inférence permet de déduire une nouvelle formule (la conclusion) à
partir d’un ensemble de formules (les prémisses ou hypothèses).
Si ψ peut se déduire grâce au système de preuves à partir des axiomes, en appliquant les règles d’inférence
du système, on note ⊢ ψ. Si ψ se déduit dans le système de preuve à partir des axiomes et des formules
dans Γ, on note Γ ⊢ ψ.
4.1 La coupure
La résolution est un système formel pour le calcul des prédicats. La méthode de la coupure est la restriction
de la résolution à la logique propositionnelle.
Ce système formel dérive de nouvelles clauses à partir de clauses données. Il n’a pas d’axiomes, et comporte
deux règles d’inférence qui sont :
R.BOUSSAHA page 6
4.1 La coupure Calcul propositionnel
1. La factorisation : On infère la clause C ∨ l à partir de la clause C ∨ l ∨ l. On présente
l’inférence dans ce cas comme suit :
C ∨l∨l
C ∨l
2. La coupure : On infère C ∨C à partir des clauses C ∨l et C ′ ∨¬l. L’inférence est représentée
′
comme suit :
C ∨l C ′ ∨ ¬l
C ∨ C′
La déduction de ⊥ à partir des clauses l et ¬l est un cas particulier de la coupure. On
représente l’inférence comme suit :
l ¬l
On utilise ce système formel pour :
1. Montrer qu’un ensemble de formules est (in)satisfaisable.
2. Montrer qu’une formule est une tautologie : on montre que sa négation est contradictoire.
3. Montrer qu’une formule φ est une conséquence logique d’un ensemble de formules Γ : on montre
que Γ ∪ {¬φ} est contradictoire.
Exercice 5 Utiliser la méthode de la coupure pour prouver ou infirmer les assertions suivantes.
1. |= ((p ⇒ q) ∧ (q ⇒ r)) ⇒ (p ⇒ r)
2. |= ((p ⇒ q) ∧ (q ⇒ p) ∧ (p ∨ q)) ⇒ (p ∧ q)
3. {p ⇒ q, q ⇒ r, p ∨ ¬r} |= p ∧ q ∧ r
R.BOUSSAHA page 7
