Logique propositionnelle
Une formule φ s’écrit en utilisant des propositions A, B, C et D. Voici sa table de vérité.
| A | B | C | D | φ |
|---|---|---|---|---|
| ⊥ | ⊥ | ⊥ | ⊥ | ⊥ |
| ⊥ | ⊥ | ⊥ | ⊤ | ⊥ |
| ⊥ | ⊥ | ⊤ | ⊥ | ⊥ |
| ⊥ | ⊥ | ⊤ | ⊤ | ⊥ |
| ⊥ | ⊤ | ⊥ | ⊥ | ⊥ |
| ⊥ | ⊤ | ⊥ | ⊤ | ⊥ |
| ⊥ | ⊤ | ⊤ | ⊥ | ⊤ |
| ⊥ | ⊤ | ⊤ | ⊤ | ⊥ |
| ⊤ | ⊥ | ⊥ | ⊥ | ⊥ |
| ⊤ | ⊥ | ⊥ | ⊤ | ⊥ |
| ⊤ | ⊥ | ⊤ | ⊥ | ⊥ |
| ⊤ | ⊥ | ⊤ | ⊤ | ⊥ |
| ⊤ | ⊤ | ⊥ | ⊥ | ⊥ |
| ⊤ | ⊤ | ⊥ | ⊤ | ⊥ |
| ⊤ | ⊤ | ⊤ | ⊥ | ⊤ |
| ⊤ | ⊤ | ⊤ | ⊤ | ⊥ |
φ est-elle une tautologie ? une contradiction ? simplement satisfiable ? Peut-on dire que φ n’est pas un théorème dans le système formel SF0 ?
En exploitant cette table de vérité, écrivez explicitement une formule dans la syntaxe de la logique propositionnelle équivalente à φ.
φ n’est ni une tautologie (car pour certaines interprétations de A, B, C et D, la formule n’est pas satisfaite), ni une contradiction (car la formule peut être satisfaite). Elle est donc simplement satisfiable. Ce n’est pas un théorème dans SF0 car les théorèmes de SF0 sont exactement les tautologies de la logique propositionnelle.
La formule φ est équivalente à B ∧ C ∧ ¬D.
Avec la méthode des tableaux, montrer que ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))) est une tautologie.
Montrer que la formule est une tautologie revient à montrer que sa négation est une contradiction. Voici l’arbre de la méthode des tableaux :
Logique des prédicats
Avec la méthode de résolution, démontrer qu’à partir des hypothèses H1, H2, H3 et H4, on peut déduire logiquement C :
- (H1) ∀x (G(x) → P(x, c1)) (c1 est une constante)
- (H2) ∀x ((F(x) ∧ E(x)) → G(x))
- (H3) ∀x∀t ((T(x,t) ∧ S(t,c2)) → F(x)) (c2 est une constante, distincte de c1)
- (H4) (E(c3) ∧ ∃t (T(c3,t) ∧ S(t,c2))) (c3 est une constante distincte de c1 et c2)
- (C) P(c3, c1)
Montrer que H1, H2, H3 et H4 implique logiquement C est équivalent à montrer que H1 ∧ H2 ∧ H3 ∧ H4 ∧ ¬C est une contradiction.
Mise sous forme prénexe :
- (H1) ∀x (G(x) → P(x, c1))
- (H2) ∀x ((F(x) ∧ E(x)) → G(x))
- (H3) ∀x∀t ((T(x,t) ∧ S(t,c2)) → F(x))
- (H4) ∃t (E(c3) ∧ (T(c3,t) ∧ S(t,c2)))
- (¬C) ¬P(c3, c1)
Mise sous forme de Skolem, avec c4 nouvelle constante. On se permet de retirer les quantificateurs car, à partir de maintenant, toutes les variables sont quantifiées universellement :
- (H1) (G(x) → P(x, c1))
- (H2) ((F(x) ∧ E(x)) → G(x))
- (H3) ((T(x,t) ∧ S(t,c2)) → F(x))
- (H4) (E(c3) ∧ (T(c3,c4) ∧ S(c4,c2)))
- (¬C) ¬P(c3, c1)
Mise sous forme normale conjonctive :
- (H1) (¬G(x) ∨ P(x, c1))
- (H2) (¬F(x) ∨ ¬E(x) ∨ G(x))
- (H3) (¬T(x,t) ∨ ¬S(t,c2) ∨ F(x))
- (H4) (E(c3) ∧ T(c3,c4) ∧ S(c4,c2))
- (¬C) ¬P(c3, c1)
Mise sous forme clausale en renommant les variables pour éviter des conflits lors de l’unification :
| (C1) | ¬G(x1) | P(x1, c1) | |
| (C2) | ¬F(x2) | ¬E(x2) | G(x2) |
| (C3) | ¬T(x3,t3) | ¬S(t3,c2) | F(x3) |
| (C4) | E(c3) | ||
| (C5) | T(c3,c4) | ||
| (C6) | S(c4,c2) | ||
| (C7) | ¬P(c3, c1) |
On applique alors la résolution de la façon suivante :
| (C8) | ¬G(c3) | obtenue par la résolution de C1 + C7 | [x1 ↦ c3] | |
| (C9) | ¬F(c3) | ¬E(c3) | obtenue par la résolution de C2 + C8 | [x2 ↦ c3] |
| (C10) | ¬F(c3) | obtenue par la résolution de C4 + C9 | ||
| (C11) | ¬T(c3,t3) | ¬S(t3,c2) | obtenue par la résolution de C3 + C10 | [x3 ↦ c3] |
| (C12) | ¬S(c4,c2) | obtenue par la résolution de C5 + C11 | [t3 ↦ c4] | |
| (C13) | ◻ | obtenue par la résolution de C6 + C12 |
On considère les prédicats suivants, avec la définition informelle qu’on leur associe :
GrapheOrienté/1:GrapheOrienté(g) est vrai si g est un graphe orienté.Sommet/2:Sommet(s,g) est vrai si s est un sommet de g.Arc/3:Arc(s1,s2,g) est vrai s’il y a un arc de s1 vers s2 dans g.Connecté/3:Connecté(s1,s2,g) est vrai si et seulement si s1 et s2 sont connectés par un chemin dans g.GrapheFortementConnexe/1:GrapheFortementConnexe(g) est vrai si g est fortement connexe.GrapheComplet/1:GrapheComplet(g) est vrai si g est un graphe complet.GrapheAcyclique/1:GrapheAcyclique(g) est vrai lorsque g est sans cycle.
Modéliser en logique des prédicats les phrases suivantes :
- Un arc dans un graphe orienté relie deux sommets de ce même graphe.
- Un sommet d’un graphe orienté est connecté à lui-même.
- Si un sommet s1 est connecté à un sommet s2 et qu’il y a un arc entre s2 et s3 alors s1 est connecté à s3.
- Un graphe orienté est fortement connexe si et seulement si tous les sommets sont connectés les uns avec les autres.
- Un graphe orienté est complet si et seulement si tous les sommets sont reliés à tous les sommets par un arc.
- Un graphe orienté est acyclique si et seulement s’il n'y a pas de chemin non vide qui connecte un sommet à lui même.
Supposons qu’on a 3 constantes c1, c2 et c3 et qu’on sait que Arc(c1,c2,c3). Sans justifier la réponse, peut-on conclure, à l’aide des formules qui précèdent, que c3 est un graphe orienté ? que c3 n’est pas un graphe fortement connexe ? que c3 n’est pas un graphe complet ? que c3 est un graphe acyclique ?
- ∀s1∀s2∀g (
Arc(s1,s2,g) → (Sommet(s1,g) ∧Sommet(s2,g))). On pourrait ajouter ∧GrapheOrienté(g). - ∀s∀g (
Sommet(s,g) →Connecté(s,s,g)) - ∀s1∀s2∀s3∀g ((
Arc(s1,s2,g) ∧Connecté(s2,s3,g)) →Connecté(s1,s3,g)) - ∀g (
GrapheFortementConnexe(g) ↔ ∀s1∀s2 ((Sommet(s1,g) ∧Sommet(s2,g)) →Connecté(s1,s2,g))) - ∀g (
GrapheComplet(g) ↔ ∀s1∀s2 ((Sommet(s1,g) ∧Sommet(s2,g)) →Arc(s1,s2,g))) - ∀g (
GrapheAcyclique(g) ↔ ∀s1∀s2 (Arc(s1,s2,g) → ¬Connecté(s2,s1,g)))
Selon la formule que l’on met en (1), on peut ou non conclure que c3 est un graphe. On ne peut pas conclure qu’il est complet ou fortement connexe ou acyclique. Pour conclure de telles choses, il faudrait savoir en plus que c3 ne contient aucun autre sommet ou arc, mais nous n’avons pas cette information.