CM7 Flashcards

1
Q

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

A
  • En minimisant le nombre d’inférences possibles avec la given clause
  • En éliminant les clauses devenues inutiles
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
2
Q

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

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
3
Q

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

A
  • 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
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
4
Q

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

A
  • 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)
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
5
Q

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

A
  • 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
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
6
Q

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

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

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

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

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

A

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é

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

Règle Res de résolution ordonnée

A

L ∨ C1 ¬L’ ∨ C2
_________________
σ(C1 ∨ C2)
où σ est le mgu entre L et L’

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
10
Q

Règle Fact de résolution ordonnée

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
11
Q

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

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
12
Q

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

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
13
Q

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

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
14
Q

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

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
15
Q

Qu’est-ce que Red(S) ?

A

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

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
16
Q

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

A

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)

17
Q

Quel est le défaut de la redondance ?

A

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

18
Q

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

A
  • 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
19
Q

Qu’est-ce que la subsomption ?

A

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

20
Q

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

A

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

21
Q

Qu’est-ce qu’une forward simplification ?

A

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

22
Q

Qu’est-ce qu’une backward simplification ?

A

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

23
Q

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

A

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

24
Q

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

A

L ∨ C1 Xσ(!L ∨ C1 ∨ C2)X
___________________________
σ(C1 ∨ C2)

25
Q

Algorithme de saturation avec simplifications

A
  • 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
26
Q
A