Examen

Logique propositionnelle

  1. Dire si les formules suivantes sont satisfiables ou non. Si oui, donner un modèle.
  1. (a ⇔ b) ⇔ ((a ⊕ c) ∨ (b ⊕ c))
  2. (p ∨ q) ⇒ (p ∧ q)
  3. (a ∧ b) ⊕ (a ∨ b)
  4. (a ⇒ c) ∧ (c ⇒ ¬a) ∧ (b ⇒ a) ∧ (a ⇒ b).
  1. On considère la formule F en FNC suivante : (x) ∧ (¬x ∨ y) ∧ (¬y ∨ z ∨ x) ∧ (z ∨ t) ∧ (¬t ∨ z)
  1. Quels sont les litéraux purs et les propagations unitaires de cette formule ?
  2. En déduire un modèle de F.
Correction
    1. Oui, a = 1, b = 1, c = 0.
    2. Oui, p = 1, q = 1.
    3. Oui, a = 1, b = 0.
    4. Oui, a = 0, c = 1, b = 0.
    1. Il y a un seul litéral pur: z. Les propagations unitaires: x, puis y.
    2. On peut donc déjà choisir x = 1, y = 1 par propagation unitaire et z = 1 puisqu’il est pur. La formule est déjà satisfaite donc on peut choisir t = 0 ou t = 1 indifféremment.

On considère la formule propositionnelle G suivante :

  1. Donnez la transformation de Tseitin de (a ⊕ b) ∨ (b ⊕ c).
  2. Donner une forme normale conjonctive de ((a ∨ ¬c) ∧ (b ∨ c)) ∧ (a ∨ (¬b ∧ c)).
Correction

  1. On introduit une nouvelle variable par porte logique:

    • (x1 ⇔ (a ⊕ b))∧
    • (x2 ⇔ (b ⊕ c))∧
    • (x3 ⇔ (x1 ∨ x2))

    Puis on récrit chaque équivalence en FNC.

    • (¬x1 ∨ a ∨ b) ∧ (¬x1 ∨ ¬a ∨ ¬b) ∧ (x1 ∨ a ∨ ¬b) ∧ (x1 ∨ ¬a ∨ b)
    • (¬x2 ∨ b ∨ c) ∧ (¬x2 ∨ ¬b ∨ ¬c) ∧ (x2 ∨ b ∨ ¬c) ∧ (x2 ∨ ¬b ∨ c)
    • (¬x3 ∨ x1 ∨ x2) ∧ (¬x1 ∨ x3) ∧ (¬x2 ∨ x3).

    La transformation de Tseitin est la conjonction des trois FNC précédentes.

  2. Pour cette formule, il suffit de développer. On remarque que le début est déjà sous forme FNC, il suffit de développer la fin. On a donc:

(a ∨ ¬c) ∧ (b ∨ c) ∧ (a ∨ ¬b) ∧ (a ∨ c).

Une clause de Horn (en logique propositionnelle) est une clause qui contient au plus un litéral positif. Une FNC est une FNC de Horn si toutes ses clauses sont des clauses de Horn.

  1. Parmi ces formules, lesquelles sont des clauses de Horn ?

    1. x ∧ ¬y ∧ ¬z
    2. w ∨ ¬x ∨ ¬t
    3. x ∨ ¬y ∨ z
    4. (x ∧ ¬y) ∨ (¬z ∧ ¬a)

  2. Montrez, en utilisant la résolution, que la FNC de Horn suivante est contradictoire : (x ∨ ¬y ∨ ¬z) ∧ (y) ∧ (¬a ∨ z) ∧ (a) ∧ (¬z ∨ ¬x)

  3. Soit F une FNC de Horn telle que toute clause de F contient au moins un litéral négatif. Montrez que F est satisfiable.

  4. Soit F une FNC de Horn qui contient une clause non-vide (de Horn) C sans litéral négatif.

    1. Combien de litéraux C peut-elle contenir ?
    2. En déduire qu’il existe une variable x de F telle que tous les modèles de F assignent la même valeur de vérité à x.

  5. En déduire un algorithme en temps polynomial pour décider si une formule de Horn est satisfiable (on expliquera l’idée générale sans donner de code et on justifiera rapidement la complexité de l’algorithme). Illustrez l’exécution de votre algorithme sur la formule donnée en question 2.

Correction
    1. N’est pas une clause (donc pas une clause de Horn non plus).
    2. C’est une clause de Horn!
    3. C’est une clause mais elle n’est pas de Horn car elle contient deux litéraux positifs.
    4. Ce n’est pas une clause (c’est par contre une FNC de Horn).

  2. On donne un nom à chaque clause de la formule originale : C1 = (x ∨ ¬y ∨ ¬z), C2 = (y), C3 = (¬a ∨ z), C4 = (a), C5 = (¬z ∨ ¬x). On peut se convaincre que la formule n’est pas satisfiable en propageant les litéraux unitaires jusqu’à arriver à une contradiction. On peut “rejouer” cette propagation unitaire en utilisant la résolution ainsi:

    • C6 = res(C3, C4) = z
    • C7 = res(C1, C5) = (¬z ∨ ¬y)
    • C8 = res(C2, C7) = ¬z
    • C9 = res(C6, C8) = ⊥, on a dérivé la clause vide.

  3. Si F est une FNC où toute clause contient au moins un litéral négatif, alors la formule est satisfait par l’assignation qui met chaque variable à 0. Donc F est satisfiable.

    1. Si C est une clause de Horn sans litéral négatif, alors elle ne contient que des litéraux positifs. Comme c’est une clause de Horn, elle ne contient par définition qu’un litéral positif, donc c’est une clause unitaire.
    2. Dans ce cas, C est une clause unitaire. Pour la satisfaire, il faut forcément assigner la seule variable qu’elle contient à 1, c’est-à-dire faire une propagation unitaire.

  5. L’algorithme est donc le suivant : si au moins une clause de F ne contient pas de litéral négatif alors, par la question 4, il existe forcément une clause unitaire. On effectue donc la propagation unitaire dans F. On obtient une nouvelle formule qui contient moins de clauses mais qui est toujours de Horn (la propagation unitaire ne peut pas ajouter des litéraux dans les clauses donc chaque clause a toujours au plus un litéral positif). Si la clause vide apparaît, on retourne UNSAT. Sinon, comme la taille de la formule diminue à chaque propagation unitaire, on arrivera à un moment au cas où : soit toute les clauses contiennent un litéral négatif, auquel cas on retourne SAT par la question 3. Soit la formule n’a pas de clauses, donc elle est trivialement satisfiable et on retourne SAT. Cet algorithme est en temps polynomial puisqu’on effectuera au plus n propagation unitaire où n est le nombre de variables et qu’on peut effectuer chaque propagation en temps |F| (nombre de litéraux dans la formule) donc un temps total de O(n|F|).

    Sur la formule de l’exemple, on aurait donc:

    • y = 1 est propagé et on a (x ∨ ¬z) ∧ (¬a ∨ z) ∧ (a) ∧ (¬z ∨ ¬x)
    • a = 1 est propagé et on a (x ∨ ¬z) ∧ (z) ∧ (¬z ∨ ¬x)
    • z = 1 est propagé et on a (x) ∧ (¬x)
    • x = 1 est propagé et on a ⊥, donc la clause vide; on retourne UNSAT.

Logique du premier ordre

Pour chaque paire de terme ci-dessous, donnez, s’il existe, un unificateur le plus général. Sinon, expliquez pourquoi un tel unificateur n’existe pas.

  1. f(u, g(t)) et f(t, g(u)).
  2. f(g(u), g(t)) et f(g(u), h(u)).
  3. f(f(g(a), b), g(b)) et f(f(b, a), g(a)).
  4. p(x, y, g(x)) et p(f(a, b), g(a), y).
Correction
  1. On applique l’algorithme de Robinson:
    • u ≃ t, g(t) ≃ g(u) en déconstruisant f,
    • u ≃ t, g(t) ≃ g(t) en propageant u ≃ t,
    • u ≃ t est donc un mgu.
  2. Les deux termes ne sont pas unifiables car :
    • g(u) ≃ g(u), g(t) ≃ h(u) en déconstruisant f,
    • on a un cas d’arrêt car g(t) et h(u) ne sont pas unifiables !
  3. Les deux termes ne sont pas unifiables:
    • f(g(a), b) ≃ f(b, a), g(b) ≃ g(a) en déconstruisant f,
    • g(a) ≃ b, b ≃ a, g(b) ≃ g(a) en déconstruisant f,
    • g(a) ≃ a, b ≃ a, g(a) ≃ g(a) en propageant b ≃ a,
    • on a un cas d’arrêt car g(a) et a ne sont pas unifiables puisque a apparaît dans g(a).
  4. Les deux termes ne sont pas unifiables:
    • x ≃ f(a, b), y ≃ g(a), g(x) ≃ y en déconstruisant p,
    • x ≃ f(a, b), y ≃ g(a), g(x) ≃ g(a) en propageant y ≃ g(a),
    • x ≃ f(a, b), y ≃ g(a), x ≃ a en déconstruisant g,
    • a ≃ f(a, b), y ≃ g(a), x ≃ a en propageant x ≃ a,
    • On a un cas d’arrêt car a et f(a, b) ne sont pas unifiables puisque a apparaît dans f(a, b).

On considère le langage du premier ordre sans constantes ni fonctions avec les prédicats suivants (les arités sont données entre parenthèses) :

Le but de cet exercice est de formaliser le fait que les prédicats ont la sémantique suivante :

  1. Écrivez des formules du premier ordre pour que toute interprétation du langage qui respectent vos formules vérifient les propriétés suivantes :
    1. Le premier argument de AEcrit doit être un titre, le second un auteur.
    2. Les deux arguments de CoAuteur sont des auteurs.
    3. Les paires de CoAuteur sont exactement les auteurs qui ont écrit un livre en commun (indiqué par le prédicat AEcrit).
  2. Donnez un modèle de la théorie définie par les trois axiomes de la question précédente (ie, une interprétation où les trois formules ci-dessus sont vraies) et où chaque prédicat est interprété sur un ensemble non-vide.
Correction
    1. ∀x∀y(AEcrit(x, y) ⇒ (Titre(x) ∧ Auteur(y))).
    2. ∀x∀y(CoAuteur(x, y) ⇒ (Auteur(x) ∧ Auteur(y))).
    3. Ici, on doit être un peu plus attentif car on a une équivalence et on veut éviter qu’un auteur soit le coauteur de lui-même : ∀x∀y(CoAuteur(x, y) ⇔ (∃tAEcrit(x, t) ∧ AEcrit(y, t) ∧ x ≠ y)).
  2. On prend le domaine D = {Alice, Bob, DatBook} et Auteur = {Alice, Bob}, Titre = {DatBook}, AEcrit = {(Alice, DatBook), (Bob, DatBook)} et CoAuteur = {(Alice, Bob)}.

On considère le language avec les prédicats PlusGrand(1), la fonction s(1) et la constante z. Donnez un modèle et un contre-modèle des formules suivantes (où aucun prédicat apparaissant dans la formule n’est interprété par l’ensemble vide) :

  1. ∃x, y(x ≠ y ∧ y ≠ z ∧ x ≠ z).
  2. ∀x(PlusGrand(x, z) ∧ ∀y(PlusGrand(x, y) ⇒ PlusGrand(s(x), y))).
  3. ∀x(x ≠ s(x)).

∀x(s(x) ≠ x ∧ PlusGrand(x, z) ∧ ∀y(PlusGrand(x, y) ⇒ (PlusGrand(s(x), y) ∧ ¬PlusGrand(y, x))))

Correction

  1. La formule dit essentiellement qu’il y a au moins trois éléments distincts dans le domaine. Donc on a le modèle: D = {0, 1, 2}, et z est interprété par 0. Contre-modèle: D = {0} et z est interprété par 0.

  2. Modèle : D = {0}, z est interprété par 0 et PlusGrand par {(0, 0)} et s: t ↦ t. Contre-modèle : D = {0, 1}, z est interprété par 0 et PlusGrand par {(0, 1)} (cela suffit à falsifier ∀x(PlusGrand(x, z)) donc nous n’avons pas besoin de donner une interprétation explicite des autres symboles).

  3. Modèle: D = {0, 1} et s: t ↦ 1 − t. Contre-modèle D = {0} et s: t ↦ t.

  4. Il y a une typo dans le sujet et cette formule n’a pas de modèle. En effet, si elle a un modèle, elle est vrai en particulier en prenant x = z. Or, on aurait PlusGrand(z, z) mais la deuxième partie de la formule impliquerait aussi ¬PlusGrand(z, z).

Si on considère plutôt la formule

∀x(s(x) ≠ x ∧ (x ≠ z ⇒ PlusGrand(x, z)) ∧ ∀y(PlusGrand(x, y) ⇒ (PlusGrand(s(x), y) ∧ ¬PlusGrand(y, x))))

on a le modèle suivant : D = ℕ, z est interprété par 0, s par s: t ↦ t + 1 et PlusGrand par {(x, y) ∣ x > y}.

Mettre sous forme prénexe les formules suivantes :

  1. ∀x(R(x)) ⇒ ∃x(S(x, x)).
  2. ∀x(T(x, z)) ∨ ∃y(S(x, y)).
  3. ∀x(S(x, z)) ∨ ¬(∃y(S(x, y)) ∧ ∃z(R(z))).
Correction
  1. ∃x∃y(R(x) ⇒ S(y, y)).
  2. ∀x0∃y(T(x0, z) ∨ S(x, y)).
  3. ∀x0∀y∀z0(S(x0, z) ∨ ¬(S(x, y) ∧ R(z0)))