Formalisation pour la programmation
CC1 logique propositionnelle

Mardi 6 octobre 2020, 15 h 45 – 17 h 15

Le livret de cours ainsi que les notes personnelles sont autorisés. Vous avez environ 45 minutes, selon le temps mis pour la partie algorithmique.

On considère la formule de logique propositionnelle ((p → (q → r)) → (r ∨ ¬p)), où p, q et r sont des propositions distinctes.

  1. À l’aide d’une table de vérité à fournir, dire si la formule est une tautologie, une contradiction, ou simplement satisfiable.
  2. Donner une interprétation qui satisfait la formule.

Table de vérité :

p q r (q → r) (p → (q → r)) (r ∨ ¬p) ((p → (q → r)) → (r ∨ ¬p))
⊥ ⊥ ⊥ ⊤ ⊤ ⊤ ⊤
⊥ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤
⊥ ⊤ ⊥ ⊥ ⊤ ⊤ ⊤
⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
⊤ ⊥ ⊥ ⊤ ⊤ ⊥ ⊥
⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤
⊤ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤
⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
  1. La formule n’est ni une tautologie (car l’une des valeurs de vérité dans la colonne de la formule est ⊥), ni une contradiction (car il y a au moins une fois ⊤ dans la colonne de la formule), donc elle est simplement satisfiable.
  2. L’interprétation I : {p ↦ ⊥, q ↦ ⊥, r ↦ ⊥} (c’est-à-dire, l’interprétation I telle que I(p) = I(q) = I(r) = ⊥) satisfait la formule. En fait, 7 des 8 interprétations possibles satisfont la formule.

Annabelle, Enrico et Fatima déjeunent ensemble. On sait que :

  1. Si Annabelle prend un dessert, Enrico en prend un aussi.
  2. Soit Enrico, soit Fatima, mais pas les deux prennent un dessert.
  3. Annabelle ou Fatima ou toutes les deux prennent un dessert.
  4. Si Fatima prend un dessert, Annabelle fait de même.

Questions :

  1. Modéliser la situation à l’aide de quatre formules en logique propositionnelle.
  2. À l’aide de la méthode des tableaux, montrer que ceci implique logiquement que Fatima ne prend pas de dessert.

On définit les propositions suivantes :

  • A : « Annabelle prend un dessert »
  • E : « Enrico prend un dessert »
  • F : « Fatima prend un dessert »

Alors, on modélise la situation comme suit :

  1. (A → E)
  2. ((E ∧ ¬F) ∨ (¬E ∧ F))
  3. (A ∨ F)
  4. (F → A)

Montrer que cette situation implique que Fatima ne prend pas de dessert, c’est-à-dire ((a) ∧ (b) ∧ (c) ∧ (d)) ⊨ ¬F, est équivalent à démontrer que la formule ((a) ∧ (b) ∧ (c) ∧ (d) ∧ ¬¬F) est une contradiction. Voici l’arbre de la méthode des tableaux :

arbre de décision Figure 1 : Arbre dont toutes les branches sont fermées, démontrant la contradiction

Construire une preuve dans SF0 permettant de montrer que la formule (q → ((¬p → ¬q) → p)) est un théorème de SF0.

Le théorème de la déduction nous indique que l’existence d’une preuve de ⊢ (q → ((¬p → ¬q) → p)) est équivalent à l’existence d’une preuve de q ⊢ ((¬p → ¬q) → p), ce qui est également équivalent à l’existence d’une preuve de q, (¬p → ¬q) ⊢ p, de par le même théorème.

On construit donc la preuve suivante :

  • c1 = qHypothèse
  • c2 = (¬p → ¬q)Hypothèse
  • c3 = ((¬p → ¬q) → (q → p))Axiome A3 avec A=p et B=q
  • c4 = (q → p)Modus ponens sur c2 et c3
  • c5 = pModus ponens sur c1 et c4