CM7

Question 1

Comment optimiser l’algorithme de saturation pour le raisonnement avec l’égalité ?

Answer 1

• En minimisant le nombre d’inférences possibles avec la given clause
• En éliminant les clauses devenues inutiles

Question 2

Comment limiter le nombre d’inférences possibles avec la given clause ?

Answer 2

En n’autorisant la résolution seulement sur les littéraux qui sont utiles pour la complétude

Question 3

Schéma de preuve de complétude de la résolution

Answer 3

• Supposer par réfutation que S’ qui contient S insatisfiable est saturé et ne contient pas la clause vide
• Construire un modèle de S’ et arriver à une contradiction

Question 4

Comment construire l’interprétation de S’ saturé dans la preuve de la complétude de la résolution ?

Answer 4

• Fixer un ordre sur les variables et l’étendre aux clauses, puis traiter les clauses dans l’ordre croissant
• Pour chaque clause, si celle-ci est déjà satisfaite par le modèle, passer à la suivante, sinon ajouter un des littéraux au modèle (de façon monotone : ajouter un littéral ne doit pas une des clauses précédentes)

Question 5

Comment la contradiction apparaît-elle dans la preuve de la complétude de la résolution ?

Answer 5

• Soit L ∨ C₁ une clause telle que L est maximum et qu’on doit ajouter C₁ à l’interprétation pour y rendre la clause vraie,
• On s’assure qu’on n’a pas déjà traité une clause ¬L ∨ C₂ où C₂ serait faux dans l’interprétation
• Puisque S’ est saturé il contient C₁ ∨ C₂ qui est plus petit que L ∨ C₁ et qui a donc déjà été traité, donc L ∨ C₁ est déjà vrai dans l’interprétaion

Question 6

Quelles conditions sur les littéraux à traiter doit-on retenir de la preuve de complétude ?

Answer 6

Puisque l’interprétation est construite avec le littéral positif maximum d’une clause ou alors un de ses littéraux négatifs quelconques, les inférences qui portent sur ces littéraux sont cruciales mais les autres peuvent être omises

Question 7

Qu’est-ce que le littéral maximum d’une clause ?

Answer 7

L est maximum dans une clause L ∨ C si L !≤ L’ pour tous les littéraux L’ de C

Question 8

Qu’est-ce qu’une fonction de sélection ?

Answer 8

Une fonction de séléection associe à chaque clause un sous-ensemble de ses littéraux tel que soit tous ses littéraux maximums sont sélectionnés, soit un littéral négatif est sélectionné

Question 9

Règle Res de résolution ordonnée

Answer 9

L ∨ C₁ ¬L’ ∨ C₂
_________________
σ(C₁ ∨ C₂)
où σ est le mgu entre L et L’

Question 10

Règle Fact de résolution ordonnée

Answer 10

L ∨ L’ ∨ C
_________________
σ(L ∨ C)
où σ est le mgu entre L et L’

Question 11

Règle de superposition positive pour la résolution ordonnée

Answer 11

s ≈ t ∨ C₁ u[s’] ≈ v ∨ C₂
_________________________
σ(u[t] ≈ v ∨ C₁ ∨ C₂)
où σ est un mgu de s et s’, σ(s) !≤ σ(t), σ(u[s’] ) !≤ σ(v) et s’ n’est pas une variable

Question 12

Règle de superposition négative pour la résolution ordonnée

Answer 12

s ≈ t ∨ C₁ u[s’] !≈ v ∨ C₂
_________________________
σ(u[t] !≈ v ∨ C₁ ∨ C₂)
où σ est un mgu de s et s’, σ(s) !≤ σ(t), σ(u[s’] ) !≤ σ(v) et s’ n’est pas une variable

Question 13

Règle de résolution d’égalité pour la résolution ordonnée

Answer 13

s !≈ s’ ∨ C
___________
σ(C)
où σ est un mgu de s et s’

Question 14

Qu’est-ce que qu’un clause redondante ?

Answer 14

Une clause C est redondante par rapport à un ensemble de clauses S s’il existe S’ ⊆ S tel que S’ |= C et ∀ C’ ∈ S’, C’ < C

Question 15

Qu’est-ce que Red(S) ?

Answer 15

L’ensemble des clauses redondantes par rapport à un ensemble de clauses S

Question 16

Qu’est-ce qu’un ensemble saturé jusqu’à redondance ?

Answer 16

Un ensemble qui contient toutes les conclusions d’inférences non-redondantes qui peuvent être faites à partir de clauses non-redondantes : Inf(S \ Red(S)) ⊆ S ∪ Red(S)

Question 17

Quel est le défaut de la redondance ?

Answer 17

Elle n’est pas décidable puisqu’il faudrait vérifier la conséquence

Question 18

Dans quels cas particuliers les redondances sont-elles exploitées ?

Answer 18

• Les tautologies : une tautologie est redondante par rapport à n’importe laquelle des clauses
• Les subsomptions : soient C et D deux clauses telles que D = σ(C’) et C’ ⊆ C, alors D est redondante par rapport à tout ensemble qui contient C

Question 19

Qu’est-ce que la subsomption ?

Answer 19

Soient C et D deux clauses telles que D = σ(C’) et C’ ⊆ C, alors C sumsume D

Question 20

Qu’est-ce qu’une inférence simplificatrice ?

Answer 20

Si lors d’une inférence, l’ajout d’une conclusion rend une prémisse redondante, on peut supprimer celle-ci

Question 21

Qu’est-ce qu’une forward simplification ?

Answer 21

La simplification ou suppresion d’une clause nouvellement créée

Question 22

Qu’est-ce qu’une backward simplification ?

Answer 22

La simplification ou suppresion d’une clause existante par une nouvellement créée

Question 23

Règle de démodulation (cas particulier de superposition)

Answer 23

s ≈ t XC[σ(s)]X
_____________
[Cσ(t)]
où σ(s) > σ(t) et σ(s ≈ t) > σ(C[σ(s)])

Question 24

Règle de subsomption/résolution (élimination contextuelle d’un littéral)

Answer 24

L ∨ C₁ Xσ(!L ∨ C₁ ∨ C₂)X
___________________________
σ(C₁ ∨ C₂)

Question 25

Algorithme de saturation avec simplifications

Answer 25

• S : clauses du problème
• Sat : ∅
• Tant que S != ∅ :
  
  • Choisir C ∈ S
  • Simplifier C par les clauses de Sat
  • Si C = □, retourner Insatisfiable
  • Si C n’est pas une tautologie et n’est pas subsumée par C’ ∈ Sat :
    
    • Supprimer et simplifier les clauses de Sat avec C
    • Déplacer les clauses simplifiées vers S
    • Faire toutes les inférences avec les prémisses dans C ∪ Sat
    • Ajouter les conclusions à S
    • Ajouter C à Sat
• Retourner Satisfiable