CM7 Flashcards
Comment optimiser l’algorithme de saturation pour le raisonnement avec l’égalité ?
- En minimisant le nombre d’inférences possibles avec la given clause
- En éliminant les clauses devenues inutiles
Comment limiter le nombre d’inférences possibles avec la given clause ?
En n’autorisant la résolution seulement sur les littéraux qui sont utiles pour la complétude
Schéma de preuve de complétude de la résolution
- 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
Comment construire l’interprétation de S’ saturé dans la preuve de la complétude de la résolution ?
- 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)
Comment la contradiction apparaît-elle dans la preuve de la complétude de la résolution ?
- Soit L ∨ C1 une clause telle que L est maximum et qu’on doit ajouter C1 à l’interprétation pour y rendre la clause vraie,
- On s’assure qu’on n’a pas déjà traité une clause ¬L ∨ C2 où C2 serait faux dans l’interprétation
- Puisque S’ est saturé il contient C1 ∨ C2 qui est plus petit que L ∨ C1 et qui a donc déjà été traité, donc L ∨ C1 est déjà vrai dans l’interprétaion
Quelles conditions sur les littéraux à traiter doit-on retenir de la preuve de complétude ?
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
Qu’est-ce que le littéral maximum d’une clause ?
L est maximum dans une clause L ∨ C si L !≤ L’ pour tous les littéraux L’ de C
Qu’est-ce qu’une fonction de sélection ?
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é
Règle Res de résolution ordonnée
L ∨ C1 ¬L’ ∨ C2
_________________
σ(C1 ∨ C2)
où σ est le mgu entre L et L’
Règle Fact de résolution ordonnée
L ∨ L’ ∨ C
_________________
σ(L ∨ C)
où σ est le mgu entre L et L’
Règle de superposition positive pour la résolution ordonnée
s ≈ t ∨ C1 u[s’] ≈ v ∨ C2
_________________________
σ(u[t] ≈ v ∨ C1 ∨ C2)
où σ est un mgu de s et s’, σ(s) !≤ σ(t), σ(u[s’] ) !≤ σ(v) et s’ n’est pas une variable
Règle de superposition négative pour la résolution ordonnée
s ≈ t ∨ C1 u[s’] !≈ v ∨ C2
_________________________
σ(u[t] !≈ v ∨ C1 ∨ C2)
où σ est un mgu de s et s’, σ(s) !≤ σ(t), σ(u[s’] ) !≤ σ(v) et s’ n’est pas une variable
Règle de résolution d’égalité pour la résolution ordonnée
s !≈ s’ ∨ C
___________
σ(C)
où σ est un mgu de s et s’
Qu’est-ce que qu’un clause redondante ?
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
Qu’est-ce que Red(S) ?
L’ensemble des clauses redondantes par rapport à un ensemble de clauses S