CM3 Flashcards
Qu’est-ce qu’une substitution ?
Une application des variables vers les termes, qui peut être étendue aux termes et aux formules, et qui définit pour chaque variable de son domaine par quel terme on le remplace dans une formule
Qu’est-ce qu’une substitution moins générale qu’une autre ?
σ’ est moins générale que σ s’il existe σ’’ telle que σσ’’ = σ’
Qu’est-ce qu’un unificateur de deux termes ?
Une substitution σ est un unificateur de deux termes s et t si et seulement si σs = σt
Théorème de l’unification de deux termes
Étant donnés deux termes s et t, soit il n’existe pas d’unificateur entre les deux, soit il existe un unificateur le plus général (mgu)
Qu’est-ce qu’un mgu ?
Une subsitution σ pour deux termes s et t telle que
- σ est un unificateur de s et t
- tout unificateur σ’ de s et t est une instance σ, c’est-à-dire qu’il existe σ’’ tel que σ’ = σσ’’
Comment calculer le mgu de deux termes ?
Avec l’algorithme de Robinson ?
Quelles sont les règles de l’algorithme de Robinson ?
- Delete
- Decompose
- Conflict
- Swap
- Eliminate
- Check
Règle Delete de l’algorithme de Robinson
G ∪ {t = t} → G
Règle Decompose de l’algorithme de Robinson
G ∪ {f(s1, …, sn) = f(t1, …, tn) } → G ∪ {s1 = t1, …, sn = tn}
Règle Conflict de l’algorithme de Robinson
G ∪ {f(s1, …, sn) = g(t1, …, tm) } → ⊥ si n != m ou f != g
Règle Swap de l’algorithme de Robinson
G ∪ {f(s1, …, sn) = x} → G ∪ {x = f(s1, …, sn)}
Règle Eliminate de l’algorithme de Robinson
G ∪ {x = t} → G[t/x] ∪ {x = t} si x !∈ t et x ∈ G
Règle Check de l’algorithme de Robinson
G ∪ {x = f(s1, …, sn)} → ⊥ si x ∈ f(s1, …, sn)
Règle sans variable libre δ∃, c frais
∃ x, P(x)
_________
P(c)
Règle sans variable libre γ¬∃
¬∃ x, P(x)
__________
¬ P(t)
Règle sans variable libre δ¬∀, c frais
¬∀ x, P(x)
__________
¬ P(c)
Règle sans variable libre γ∀
∀ x, P(x)
_________
P(t)
Règle destructive δ∃, f frais, Xi variables libres
∃ x, P(x)
__________________________________________
P(f (X1, …, Xn))
Règle non-destructive δ∃, f frais, Xi variables libres
∃ x, P(x)
__________________________________________
P(f (X1, …, Xn))
Règle non-destructive avec ϵ-termes δ∃, f frais, Xi variables libres
∃ x, P(x)
___________
P(ϵ(x), P(x))
Règle destructive δ¬∀, f frais, Xi variables libres
¬∀ x, P(x)
__________________________________________
¬P(f (X1, …, Xn))
Règle non-destructive δ¬∀, f frais, Xi variables libres
¬∀ x, P(x)
__________________________________________
¬P(f (X1, …, Xn))
Règle non-destructive avec ϵ-termes δ¬∀, f frais, Xi variables libres
¬∀ x, P(x)
_______________
¬P(ϵ(x), ¬P(x))
Règle destructive γ¬∃M
¬∃ x, P(x)
__________
¬P(X)
Règle non-destructive γ¬∃M
¬∃ x, P(x)
__________
¬P(X)
Règle destructive γ∀M
∀ x, P(x)
__________
P(X)
Règle non-destructive γ∀M
∀ x, P(x)
__________
P(X)
Règle destructive γ¬∃inst
¬∃ x, P(x)
__________
¬P(t)
Règle non-destructive γ¬∃inst
¬∃ x, P(x)
__________
¬P(t)
Règle destructive γ¬∀inst
∀ x, P(x)
__________
P(t)
Règle non-destructive γ¬∀inst
∀ x, P(x)
__________
P(t)
Règle destructive ⊙
Appliquer σ s’il existe deux littéraux K et ¬L dans la branche tels que σ = mgu(K, L)
Théorème de Herbran-Skolem
Pour toute formule F :
- Il existe une formule existentielle F’ telle que F’ est valide si et seulement F l’est
- Il existe une formule universelle F’ telle que F’ est valide si et seulement F l’est
Fonctions de skolémisation
- Si F est atomique, s(F) = F
- s(F ∧/∨ G) = s(F) ∧/∨ s(G)
- s(¬F) = ¬h(F)
- s(F ⇒ G) = h(F) ⇒ s(G)
- s(∀ x, F) = s(F)
- s(∃ x, F) = s(F)[f(x1, …, xn)/x] où x1, …, xn sont les variables libres de ∃ x, F
Fonctions d’herbrandisation
- Si F est atomique, h(F) = F
- h(F ∧/∨ G) = h(F) ∧/∨ h(G)
- h(¬F) = ¬s(F)
- h(F ⇒ G) = s(F) ⇒ h(G)
- h(∃ x, F) = h(F)
- h(∀ x, F) = h(F)[f(x1, …, xn)/x] où x1, …, xn sont les variables libres de ∀ x, F
Étapes de la méthode de Résolution au premier ordre
- Nier la formule initiale
- Skolémoser la formule niée
- Clausifier la formule skolémisée sans ses quantificateurs
- Appliquer la règle de résolution sur les clausses de Sat et mettre les résolvantes dans S
Règle de résolution au premier ordre
A∨C | ¬B∨D (avec σ(A) = σ(B))
_______________________________
σ(C) ∨ σ(D)
Règle de factorisation positive
A∨B∨C (avec σ(A) = σ(B))
__________________________
σ(B) ∨ σ(C)
Règle de factorisation négative
¬A∨¬B∨C (avec σ(A) = σ(B))
_____________________________
¬σ(B) ∨ σ(C)