Formalisation pour la programmation
CC2 logique des prédicats

Mardi 9 novembre 2021, 16 h 15 – 17 h 00

Le livret de cours et les notes personnelles sont autorisés. Vous avez 45 minutes. Les étudiants composant à distance doivent envoyer une photo de leur travail à antoine.zimmermann@emse.fr et christopher.leturc@emse.fr.

Soit P un prédicat unaire et x une variable. Montrer, en utilisant la méthode des tableaux, que la formule ∀x P(x) a pour conséquence logique la formule ∃x P(x).

La question équivaut à montrer que la formule (∀x P(x) ∧ ¬∃x P(x)) est une contradiction. On applique alors la méthode des tableaux sur cette formule.

tableau pour la formule ∀x P(x)∧¬∃x P(x)
Figure 1: Le tableau pour le formule ∀x P(x) ∧ ¬∃x P(x)

Exprimer en logique des prédicats les affirmations suivantes :

  1. Tous les êtres humains ont un cœur et un cerveau ;
  2. Tous les êtres humains ont un parent qui est un être humain ;
  3. Tous les parents d’être humain sont des êtres humains.

Il y a plusieurs possibilités permettant d’effectuer des déductions plus ou moins précises. En cherchant à bien détailler les entités et leurs relations, on peut par exemple introduire les prédicats :

  • Humain/1 : signifie que l’entité en argument est un être humain ;
  • Cœur/1 : signifie que l’entité en argument est un cœur ;
  • Cerveau/1 : signifie que l’entité en argument est un cerveau ;
  • possède/2 : signifie que le premier argument possède le second argument ;
  • aPourParent/2 : signifie que le premier argument a un parent qui est le second argument.

Le prédicat possède peut être ambigu car on peut posséder un cerveau dans un bocal de formol sur une étagère, ce qui est différent d’avoir un cerveau qui fait partie intégrante de son corps. On aurait pu introduire estComposéDe ou aCommePartie, etc. En utilisant ces prédicats, on peut exprimer les formules comme suit :

  1. ∀x (Humain(x) → (∃y (possède(x,y) ∧ Cœur(y)) ∧ ∃z (possède(x,z) ∧ Cerveau(z))))
    ou bien, sous forme prénexe : ∀x∃y∃z (Humain(x) → (possède(x,y) ∧ Cœur(y) ∧ possède(x,z) ∧ Cerveau(z)))
  2. ∀x (Humain(x) → ∃y (aPourParent(x,y) ∧ Humain(y)))
    ou bien, sous forme prénexe : ∀x∃y (Humain(x) → (aPourParent(x,y) ∧ Humain(y)))
  3. ∀x (Humain(x) → ∀y (aPourParent(x,y) → Humain(y)))
    ou bien, sous forme prénexe et un peu modifiée : ∀x∀y ((Humain(x) ∧ aPourParent(x,y)) → Humain(y)).

On considère les prédicats binaires suivants :

  • PO/2 (« is Part Of ») : indique qu’une région de l’espace (ou une zone géographique) est une partie d’une autre région de l’espace plus grande. Par exemple, on pourra exprimer que Saint-Étienne fait partie de la région Auvergne-Rhône-Alpes en écrivant PO(Saint-Étienne,Auvergne-Rhône-Alpes) ;
  • DF/2 (« is Disjoint From ») : indique qu’une région de l’espace (ou une zone géographique) est complètement séparée et ne recoupe pas une autre région de l’espace. Par exemple, on pourra exprimer que Saint-Étienne est disjoint de Paris en écrivant DF(Saint-Étienne,Paris).

On introduit aussi les constantes suivantes : G pour désigner la Guyane française, F pour désigner la France, E pour désigner l’Europe et SA pour désigner l’Amérique du sud.

Montrer, en utilisant la méthode de résolution, que A1 ∧ A2 ∧ F1 ∧ F2 ∧ F3 ∧ F4 est une contradiction :

  • (A1) ∀x∀y (DF(x,y) → ∀z (¬PO(z,x) ∨ ¬PO(z,y))) – deux régions disjointes ne peuvent contenir une partie commune ;
  • (A2) ∀x∀y∀z ((PO(x,y) ∧ PO(y,z)) → PO(x,z)) – la relation de sous-partie est transitive.
  • (F1) PO(G,F) – la Guyane fait partie de la France ;
  • (F2) PO(F,E) – la France fait partie de l’Europe ;
  • (F3) PO(G,SA) – la Guyane fait partie de l’Amérique du sud ;
  • (F4) DF(E,SA) – l’Europe et l’Amérique du sud sont des régions disjointes.

On veillera à bien détailler les étapes de la méthode.

Mise sous forme prénexe :

  • (A1)∀x∀y∀z (DF(x,y) → (¬PO(z,x) ∨ ¬PO(z,y)))
  • (A2)∀x∀y∀z ((PO(x,y) ∧ PO(y,z)) → PO(x,z))
  • (F1)PO(G,F)
  • (F2)PO(F,E)
  • (F3)PO(G,SA)
  • (F4)DF(E,SA)

Toutes les formules sont déjà sous forme de Skolem. À partir de maintenant, on se permet d’omettre les quantificateurs car toutes les variables sont quantifiées universellement.

Mise sous forme normale conjonctive :

  • (A1)(¬DF(x,y) ∨ ¬PO(z,x) ∨ ¬PO(z,y))
  • (A2)(¬PO(x,y) ∨ ¬PO(y,z) ∨ PO(x,z))
  • (F1)PO(G,F)
  • (F2)PO(F,E)
  • (F3)PO(G,SA)
  • (F4)DF(E,SA)

Mise sous forme clausale et renommage des variables pour éviter des conflits de noms lors de l’unification :

(C1) ¬DF(x1,y1) ¬PO(z1,x1) ¬PO(z1,y1)
(C2) ¬PO(x2,y2) ¬PO(y2,z2) PO(x2,z2)
(C3) PO(G,F)
(C4) PO(F,E)
(C5) PO(G,SA)
(C6) DF(E,SA)

On applique alors la résolution de la façon suivante :

(C7) ¬PO(z1,E) ¬PO(z1,SA) obtenue par la résolution de C1 + C6 [x1 ↦ E, y1 ↦ SA]
(C8) ¬PO(F,z2) PO(G,z2) obtenue par la résolution de C3 + C2 [x2 ↦ G, y2 ↦ F]
(C9) PO(G,E) obtenue par la résolution de C8 + C4 [z2 ↦ E]
(C10) ¬PO(G,SA) obtenue par la résolution de C7 + C9 [z1 ↦ G]
(C11) ◻ obtenue par la résolution de C5 + C10