CM3

Question 1

Qu’est-ce qu’une substitution ?

Answer 1

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

Question 2

Qu’est-ce qu’une substitution moins générale qu’une autre ?

Answer 2

σ’ est moins générale que σ s’il existe σ’’ telle que σσ’’ = σ’

Question 3

Qu’est-ce qu’un unificateur de deux termes ?

Answer 3

Une substitution σ est un unificateur de deux termes s et t si et seulement si σs = σt

Question 4

Théorème de l’unification de deux termes

Answer 4

É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)

Question 5

Qu’est-ce qu’un mgu ?

Answer 5

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 σ’ = σσ’’

Question 6

Comment calculer le mgu de deux termes ?

Answer 6

Avec l’algorithme de Robinson ?

Question 7

Quelles sont les règles de l’algorithme de Robinson ?

Answer 7

• Delete
• Decompose
• Conflict
• Swap
• Eliminate
• Check

Question 8

Règle Delete de l’algorithme de Robinson

Answer 8

G ∪ {t = t} → G

Question 9

Règle Decompose de l’algorithme de Robinson

Answer 9

G ∪ {f(s₁, …, s_n) = f(t₁, …, t_n) } → G ∪ {s₁ = t₁, …, s_n = t_n}

Question 10

Règle Conflict de l’algorithme de Robinson

Answer 10

G ∪ {f(s₁, …, s_n) = g(t₁, …, t_m) } → ⊥ si n != m ou f != g

Question 11

Règle Swap de l’algorithme de Robinson

Answer 11

G ∪ {f(s₁, …, s_n) = x} → G ∪ {x = f(s₁, …, s_n)}

Question 12

Règle Eliminate de l’algorithme de Robinson

Answer 12

G ∪ {x = t} → G[t/x] ∪ {x = t} si x !∈ t et x ∈ G

Question 13

Règle Check de l’algorithme de Robinson

Answer 13

G ∪ {x = f(s₁, …, s_n)} → ⊥ si x ∈ f(s₁, …, s_n)

Question 14

Règle sans variable libre δ_∃, c frais

Answer 14

∃ x, P(x)
_________
P(c)

Question 15

Règle sans variable libre γ_¬∃

Answer 15

¬∃ x, P(x)
__________
¬ P(t)

Question 16

Règle sans variable libre δ_¬∀, c frais

Answer 16

¬∀ x, P(x)
__________
¬ P(c)

Question 17

Règle sans variable libre γ_∀

Answer 17

∀ x, P(x)
_________
P(t)

Question 18

Règle destructive δ_∃, f frais, X_i variables libres

Answer 18

∃ x, P(x)
__________________________________________
P(f (X₁, …, X_n))

Question 19

Règle non-destructive δ_∃, f frais, X_i variables libres

Answer 19

∃ x, P(x)
__________________________________________
P(f (X₁, …, X_n))

Question 20

Règle non-destructive avec ϵ-termes δ_∃, f frais, X_i variables libres

Answer 20

∃ x, P(x)
___________
P(ϵ(x), P(x))

Question 21

Règle destructive δ_¬∀, f frais, X_i variables libres

Answer 21

¬∀ x, P(x)
__________________________________________
¬P(f (X₁, …, X_n))

Question 22

Règle non-destructive δ_¬∀, f frais, X_i variables libres

Answer 22

¬∀ x, P(x)
__________________________________________
¬P(f (X₁, …, X_n))

Question 23

Règle non-destructive avec ϵ-termes δ_¬∀, f frais, X_i variables libres

Answer 23

¬∀ x, P(x)
_______________
¬P(ϵ(x), ¬P(x))

Question 24

Règle destructive γ_¬∃M

Answer 24

¬∃ x, P(x)
__________
¬P(X)

Question 25

Règle non-destructive γ_¬∃M

Answer 25

¬∃ x, P(x)
__________
¬P(X)

Question 26

Règle destructive γ_∀M

Answer 26

∀ x, P(x)
__________
P(X)

Question 27

Règle non-destructive γ_∀M

Answer 27

∀ x, P(x)
__________
P(X)

Question 28

Règle destructive γ_¬∃inst

Answer 28

¬∃ x, P(x)
__________
¬P(t)

Question 29

Règle non-destructive γ_¬∃inst

Answer 29

¬∃ x, P(x)
__________
¬P(t)

Question 30

Règle destructive γ_¬∀inst

Answer 30

∀ x, P(x)
__________
P(t)

Question 31

Règle non-destructive γ_¬∀inst

Answer 31

∀ x, P(x)
__________
P(t)

Question 32

Règle destructive ⊙

Answer 32

Appliquer σ s’il existe deux littéraux K et ¬L dans la branche tels que σ = mgu(K, L)

Question 33

Théorème de Herbran-Skolem

Answer 33

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

Question 34

Fonctions de skolémisation

Answer 34

• 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(x₁, …, x_n)/x] où x₁, …, x_n sont les variables libres de ∃ x, F

Question 35

Fonctions d’herbrandisation

Answer 35

• 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(x₁, …, x_n)/x] où x₁, …, x_n sont les variables libres de ∀ x, F

Question 36

Étapes de la méthode de Résolution au premier ordre

Answer 36

• 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

Question 37

Règle de résolution au premier ordre

Answer 37

A∨C | ¬B∨D (avec σ(A) = σ(B))
_______________________________
σ(C) ∨ σ(D)

Question 38

Règle de factorisation positive

Answer 38

A∨B∨C (avec σ(A) = σ(B))
__________________________
σ(B) ∨ σ(C)

Question 39

Règle de factorisation négative

Answer 39

¬A∨¬B∨C (avec σ(A) = σ(B))
_____________________________
¬σ(B) ∨ σ(C)