CM2 Flashcards

1
Q

Méthode de résolution naïve en logique propositionnelle

A

Essayer toutes les assignations possibles pour les variables (⊤,⊥)

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

Qu’est-ce qu’une proposition valide ?

A

Une proposition qui est vraie pour toute assignation possible des variables

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

Qu’est-ce qu’une proposition insatisfiable ?

A

Une proposition qui est fausse pour toute assignation possible des variables

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

Qu’est-ce qu’une proposition non-valide ?

A

Une proposition qui est fausse pour certaines assignations possibles des variables

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

Qu’est-ce qu’une proposition satisfiable ?

A

Une proposition qui est vraie pour certaines assignations possibles des variables

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

Étapes de la méthode DPLL (Davis-Putnam-Logemann-Loveland)

A
  • Nier la formule initiale
  • Clausifier la formule niée
  • Appliquer les simplifications possibles
  • Appliquer l’algorithme DPLL
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

Principe du “Splitting” (DPLL)

A
  • S[A := ⊤] est S dans lequel on a supprimé toutes les clauses contenant A et supprimé ¬A des autres clauses
  • S[A := ⊥] est S dans lequel on a supprimé toutes les clauses contenant ¬A et supprimé A des autres clauses
  • S est insatisfiable si S[A := ⊤] ∧ [A := ⊤] l’est
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

Simplification possibles (DPLL)

A
  • Clauses unitaires à traiter en priorité
  • Clauses pures à traiter en priorité
  • Tautologies à supprimer
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

Algorithme DPLL

A
  • Si S = ∅ :
    • Retourner satisfiable
  • ∅ ∈ S :
    • Retourner insatisfiable
  • Si clause unitaire U (resp. ¬U) ∈ S :
    • Renvoyer DPLL(S[U := ⊤ (resp. ⊥)])
  • Si P (resp. ¬P) pur ∈ S :
    • Renvoyer DPLL(S[P := ⊤ (resp. ⊥)])
  • Choisir A ∈ S :
  • Renvoyer DPLL(S[A := ⊤]) ∨ DPLL(S[A := ⊥])
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
10
Q

Étapes de la méthode de Résolution propositionnelle

A
  • Nier la formule initiale
  • Clausifier la formule niée
  • Appliquer la règle de résolution sur les clausses de Sat et mettre les résolvantes dans S
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
11
Q

Règle de résolution

A

C∨A | ¬A∨C’
______________
C∨C’

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

Algorithme de Résolution

A
  • Sat = ∅
  • Tant que S != ∅
    • Choisir C une clause de S
    • Enlever C de S
    • Si C = ∅ :
      • Renvoyer insatisfiable
    • Si C ∈ Sat ou C est une tautologie
      • Passer à la clause suivante
    • Appliquer la résolution sur C et toutes les clauses de Sat
      • Rajouter toutes les résolvantes à S
      • Rajouter C à Sat
  • Renvoyer satisfiable
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
13
Q

Étapes de la méthode des tableaux

A
  • Nier la formule initiale
  • Appliquer des règles jusqu’à clore toutes les branches
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
14
Q

Règle ⊙

A


___

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

Règle ⊙¬⊤

A

¬⊤
____

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

Règle ⊙

A

¬P P
_____

17
Q

Règle ᬬ

A

¬¬P
_____
P

18
Q

α

A

P∧Q
______
P, Q

19
Q

β¬∧

A

¬(P∧Q)
________
¬P ∣ ¬Q

20
Q

β

A

P∨Q
_____
P ∣ Q

21
Q

α¬∨

A

¬(P∨Q)
________
¬P, ¬Q

22
Q

β

A

P⇒Q
______
¬P ∣ Q

23
Q

α¬⇒

A

¬(P⇒Q)
________
P, ¬Q

24
Q

β

A

P⇔Q
_____________
¬P, ¬Q ∣ P, Q

25
Q

β¬⇔

A

¬(P⇔Q)
_____________
¬P, Q ∣ P, ¬Q