TP 5 : Révision

1. On met V_A sous forme conjonctive en distribuant le ∧ sur le ∨: V_A est équivalent à (H_A∨¬H_A) ∧ (H_A∨F_A) ∧ (¬H_A∨¬F_A) ∧ (F_A∨¬F_A). En enlevant les clauses triviales, on trouve V_A équivalent à (H_A∨F_A) ∧ (¬H_A∨¬F_A). Par symmétrie, V_B est équivalent à (H_B∨F_B) ∧ (¬H_B∨¬F_B).

Quand à P, on a :

• H_A ⇔ H_B équivalent à H_A ⇒ H_B ∧ H_B ⇒ H_A, lui-même équivalent à (¬H_A∨H_B) ∧ (¬H_B∨H_A).

• Par énumération des modèles, on a V_A ⇔ V_B équivalent à (¬H_A∨F_A∨H_B∨F_B) ∧ (¬H_A∨¬F_A∨H_B∨¬F_B) ∧ (H_A∨F_A∨¬H_B∨F_B) ∧ (H_A∨¬F_A∨¬H_B∨¬F_B) ∧ (H_A∨¬F_A∨H_B∨F_B) ∧ (H_A∨F_A∨H_B∨¬F_B) ∧ (¬H_A∨¬F_A∨¬H_B∨F_B) ∧ (¬H_A∨F_A∨¬H_B∨¬F_B)

• V_B ⇔ F_A équivalent à (¬V_B∨F_A) ∧ (¬F_A∨V_B). ¬V_B est directement sous forme clausal après application des lois de De Morgan, on peut donc distribuer F_A dans chacune des clause. Pour ¬F_A ∨ V_B, on distribue ¬F_A dans chacune des clauses de la forme clausale de F_A. On obtient donc (F_A∨¬H_B∨F_B) ∧ (F_A∨H_B∨¬F_B) ∧ (¬F_A∨H_B∨F_B) ∧ (¬F_A∨¬H_B∨¬F_B)

Donc la forme clausale de P est la conjonction de ces trois formes clausales.

On peut enlever certaines clauses qui sont incluses dans d’autres (donc si la plus petite est satisfaite, la plus grande aussi). On obtient ainsi :

(¬H_A∨H_B) ∧ (¬H_B∨H_A) ∧ (H_A∨¬F_A∨H_B∨F_B) ∧ (¬H_A∨¬F_A∨¬H_B∨F_B) ∧ (¬H_A∨F_A∨¬H_B∨¬F_B) ∧ (F_A∨¬H_B∨F_B) ∧ (F_A∨H_B∨¬F_B) ∧ (¬F_A∨H_B∨F_B) ∧ (¬F_A∨¬H_B∨¬F_B)

2. On peut dériver une contradiction (la clause vide) ainsi :

• Les clauses H_B et (F_A∨¬H_B∨F_B) permettent de dériver la clause (F_A∨F_B).
• Les clauses H_B et (¬F_A∨¬H_B∨¬F_B) permettent de dériver la clause (¬F_A∨¬F_B).
• (¬H_A∨F_A∨¬H_B∨¬F_B) et H_A puis H_B (deux étapes de résolutions) donnent F_A ∨ ¬F_B
• (¬H_A∨¬F_A∨¬H_B∨F_B) et H_A puis H_B (deux étapes de résolutions) donnent ¬F_A ∨ F_B
• F_A ∨ ¬F_B et F_A ∨ F_B permettent de dériver F_A
• ¬F_A ∨ ¬F_B et ¬F_A ∨ F_B permettent de dériver ¬F_A
• F_A et ¬F_A permettent de dériver la clause vide, contradiction !

1. L’indication 1 correspond à la proposition P₁ définie par V₂^I.

L’indication 2 correspond à la proposition P₂ définie par (V₁^N⇒M₁^B) ∧ (V₂^N⇒M₂^B) ∧ (V₃^N⇒M₃^B).

L’indication 3 correspond à la proposition P₃ définie par ¬V₁^E ∧ V₂^E ⇒ M₁^R ∧ V₃^E ⇒ M₂^R.

2. Le fait que la maison i a exactement une couleur s’exprime par C_i définie par (M_i^R⇒(¬M_i^B∧¬M_i^V)) ∧ (M_i^B⇒(¬M_i^R∧¬M_i^V)) ∧ (M_i^V⇒(¬M_i^B∧¬M_i^R)) ∧ (M_i^R∨M_i^B∨M_i^V).

Chaque maison a exactement une couleur se traduit donc par C définie comme C₁ ∧ C₂ ∧ C₃.

3. Le fait que dans la maison i, il y a exactement un habitant d’une seule nationalité se traduit par la proposition N_i définie par (V_i^N⇒(¬V_i^E∧¬V_i^I)) ∧ (V_i^I⇒(¬V_i^E∧¬V_i^N)) ∧ (V_i^E⇒(¬V_i^N∧¬V_i^I)) ∧ (V_i^I∨V_i^E∨V_i^N).

Le fait que dans chaque maison, il y a exactement un habitant d’une seule nationalité se traduit par la proposition N définie par N₁ ∧ N₂ ∧ N₃.

4. On en déduit que les solutions du problème s’expriment par la proposition P définie par P₁ ∧ P₂ ∧ P₃ ∧ C ∧ N.

Pour des raisons esthétiques et pédagogiques, on va éviter les modèles où le domaine est vide.

1. Cette formule exprime intuitivement le fait que P est inclus dans Q.

• Modèle M : U = {0}, P^M = ∅, Q^M = {0}.
• Contre-modèle C : U = {0}, P^C = {0}, Q^M = ∅.

2. Cette formule exprime intuitivement le fait que tout élément x est en relation avec au moins un y dans P.

• Modèle M : U = {0}, P^M = {(0,0)}.
• Contre-modèle C : U = {0}, P^C = ∅.

Si on veut éviter d’utiliser l’ensemble vide, on peut aussi considérer le contre-modèle K défini par U = {0, 1}, P^K = {(0,0)}. En effet, pour x = 1, on ne peut pas trouver de y telle que (1,y) ∈ P^K.

3. Cette formule exprime intuitivement le fait qu’il y a au moins un y qui est en relation avec tous les éléments du domaine.

• Modèle M : U = {0}, P^M = {(0,0)}.
• Contre-modèle C : U = {0}, P^C = ∅.

On peut aussi regarder le contre-modèle K : U = {0, 1}, P^K = {(0,0)} et le modèle N sur le même domaine mais avec P^N = {(0,0), (1,0)}.

On peut se convaincre que tout modèle de (3) est un modèle de (2) (exercice bonus : le prouver en calcul des séquents pour plus de fun !). Cela veut dire, en particulier, que (2) est une conséquence logique de (3).

Le contraire n’est pas vrai cependant. On peut trouver un modèle de (2) qui n’est pas un modèle de (3). Par exemple J, défini sur le domaine U = {0, 1} et P^J = {(0,0), (1,1)}.

4. Intuitivement, cette formule exprime qu’il y a au moins trois éléments distincts dans P. On aura donc :

• Modèle M : U = {0, 1, 2}, P^M = U.
• Contre-modèle C : U = {0}, P^C = U.

1. ∀x(Ami(Alice,x)⇒Ami(Bob,x)).
2. ∃x∃y∃z(x≠y∧y≠z∧x≠z∧Ami(Alice,x)∧Ami(Alice,y)∧Ami(Alice,z)) où on écrit x ≠ y pour la formule ¬(x=y).
3. ∀x∃a∃e∃n(Ami(x,a)∧Ennemi(x,e)∧¬Ami(x,n)∧¬Ennemi(x,n)). Remarquez que pour simplifier, j’ai choisi ici la forme normale prénexe, mais on aurait pu avoir une forme plus élégante où les quantificateurs existentiels ont une portée ne contenant que les atomes qui les font intervenir.
4. ∃z∃u(x<y∧R(x,z)∧S(y,u)).
5. ∃z(R(x,y,z)∧¬S(x,y,z)).

Variables libres {x}.

Forme prénexe :

Variables libres {x}.

Forme prénexe, attention à la capture, on renomme la variable x liée en x₀. De plus, le quantificateur universel sur z étant à gauche de l’implication, il devient existentiel.

3. Presque la même formule mais cette fois-ci, on risque une capture sur y!

Variables libres {x, y}.

Forme prénexe, attention aux captures, on renomme les variables x, y liées en x₀, y₀. De plus, le quantificateur universel sur z étant à gauche de l’implication, il devient existentiel.

1. Pour unifier ces termes, on doit unifier x=_?h(y) et h(y)=_?y. On échoue immédiatement car h(y)=_?y est un cas d’arrêt de l’algorithme de Robinson, ces termes n’étant trivialement pas unifiables.

2. On doit unifier x=_?h(y), h(y)=_?h(x), s(x,z)=_?s(h(y),x). En remplaçant x par h(y) dans tous les termes, on doit unifier x=_?h(y), h(y)=_?h(h(y)), s(h(y),z)=_?s(h(y),h(y)). On déconstruit h(y)=_?h(h(y)), on doit donc unifier : x=_?h(y), y=_?h(y), s(h(y),z)=_?s(h(y),h(y)). On échoue pour les mêmes raisons qu’au-dessus.

3. On doit unifier g(x,f(y),f(z))=_?g(f(y),z,t). On déconstruit g et on doit unifier x=_?f(y), f(y)=_?z, f(z)=_?t. On remplace z par f(y) et on se retrouve à unifier : x=_?f(y), z=_?f(y), t=_?f(f(y)). On a trouvé un unificateur le plus général !