0% ont trouvé ce document utile (0 vote)
134 vues2 pages

Logique et Unification en Calcul des Prédicats

Transféré par

Noupa mike mike
Copyright
© © All Rights Reserved
Nous prenons très au sérieux les droits relatifs au contenu. Si vous pensez qu’il s’agit de votre contenu, signalez une atteinte au droit d’auteur ici.
Formats disponibles
Téléchargez aux formats PDF, TXT ou lisez en ligne sur Scribd
0% ont trouvé ce document utile (0 vote)
134 vues2 pages

Logique et Unification en Calcul des Prédicats

Transféré par

Noupa mike mike
Copyright
© © All Rights Reserved
Nous prenons très au sérieux les droits relatifs au contenu. Si vous pensez qu’il s’agit de votre contenu, signalez une atteinte au droit d’auteur ici.
Formats disponibles
Téléchargez aux formats PDF, TXT ou lisez en ligne sur Scribd

Université Paris Diderot - Licence 3 Année 2014–2015

TD de Logique no 12

Révision

Exercice 1 [Modélisation et preuve] Formaliser les phrases suivantes en calcul des prédicats
(Commencer en donnant les prédicats utilisés) :
1. Chaque garçon ou fille est un enfant (Every boy or girl is a child).
2. Chaque enfant reçoit une poupée ou un train (Every child gets a doll or a train).
3. Aucun garçon ne reçoit de train (No boy gets a train).
4. Si aucun enfant ne reçoit de poupée, alors il n’y a pas de garçons (If no child gets a doll,
then there are no boys).
Montrer avec la méthode de votre choix que 4. est une conséquence logique de 1. à 3.

Exercice 2 [Unification] Pour les problèmes d’unification suivants donner un unificateur prin-
cipal s’il existe, ou indiquer qu’il n’y en a pas. u, x, y, z sont des variables, et a, b, c des constantes.
Détailler l’application de l’algorithme d’unification pour chaque problème.
.
1. p(f (y, z), c, x) = p(f (z, g(b, x)), c, g(b, y))
.
2. p(y, x, y) = p(a, z, z)
.
3. p(f (y), y) = p(u, f (u))

Exercice 3 [Résolution] Montrer en utilisant la résolution que l’ensemble de clauses suivant


est contradictoire (x, y, z, u sont des variables, a, b des constantes, f un symbole de fonction
d’arité 2, g un symbole de fonction d’arité 1 et p, q, r des symboles de prédicats) :

{q(y) ∨ p(g(y)) ∨ r(f (y, z)), p(a), ¬p(x) ∨ ¬q(f (x, b)), ¬p(g(f (g(f (a, b)), b))), ¬r(u)}

Exercice 4 [Mise sous forme causale - Résolution]


1. Mettre en forme clausale l’ensemble de formules suivant :
(a) φ1 = ∀x (V (x) → (C(x) ∨ (∃y(A(x, y) ∧ P (y)))))
(b) φ2 = ∃x (E(x) ∧ V (x) ∧ ¬(∃y A(x, y) ∧ (¬E(y))))
(c) φ3 = ∀x (E(x) → ¬C(x))
(d) φ4 = ¬∃x (E(x) ∧ P (x))
2. Appliquez la résolution à l’ensemble de clauses obtenu afin de montrer que la conjonction
des énoncés (a) à (c) entraîne la négation de l’énoncé (d), i.e. :

{φ1 , φ2 , φ3 } ` ∃x(E(x) ∧ P (x))

Exercice 5 [Gentzen] On considère un langage du premier ordre, où p/1 et q/1 sont des sym-
boles de prédicat. En utilisant le système de Gentzen pour le calcul des prédicats, démontrer que
les formules suivantes sont valides :

1
1. (∀x p(x)) → (∃x p(x))
2. (∀x p(x)) → (∀y p(y))
3. (∃x (p(x) ∧ q(x))) → ∃x p(x)
4. (∀x (p(x) ∧ q(x))) → ∀x p(x)
5. (∀x (p(x) ∧ q(x))) → (∀x (p(x) ∨ q(x)))

Exercice 6 [Sémantique] On considère une signature Σ avec ΣF = {a/0, b/0, g/2} et ΣP =


{p/2, r/1}. Soit l’interprétation I donnée par le domaine D = {0, 1, 2, 3, 4}, I(a) = 3, I(b) = 4,
I(g)(x, y) = (x + y) mod 4 (u mod 4 est le reste de la division entière de u par 4), I(p) =
{(0, 1), (1, 2), (2, 3), (3, 1), (4, 4)} et I(r) = {2, 4}.
Indiquer si I est un modèle pour les formules suivantes. Justifier votre réponse pour 4.
1. ∀x (r(x) ∧ r(b))
2. ∃x (p(x, a) ∧ r(x))
3. ∀x ∃y ((p(x, y) ∧ r(x)) → q(g(x, y)))
4. ∃y ((∀x p(x, y)) → (∀x r(x)))
I n’est pas un modèle de la formule A = ∀x ∀y (p(x, y) → p(x, g(x, y))). Modifier I pour qu’elle
devienne un modèle de A.

Exercice 7 [Unification] Au lieu d’unifier deux termes, on souhaite unifier un ensemble de


termes. Soient X un ensemble de variables et Σ une signature. Étant donné un ensemble S ⊆ TΣ,X
(de taille ≥ 2) de termes, on veut obtenir un unificateur σ de sorte qu’il y ait un terme t ∈ TΣ,X tel
que pour tout t0 ∈ S, on a σ(t0 ) = t (égalité syntaxique). Donner un algorithme d’unification (qui
renvoie un σ s’il existe ou échec sinon) pour ce problème. Exemple : pour {g(x, y), g(a, u), g(z, b)},
l’algorithme renvoie σ = {x ← a, y ← b, u ← b, z ← a}. En quoi cette notion d’unification peut
être utile dans la résolution ?

Vous aimerez peut-être aussi