CM6

Question 1

Qu’est-ce que le problème du raisonnement avec égalité ?

Answer 1

On considère une conjonction d’égalités et d’inégalités et on se demande si cette conjonction est satisfiable au sens de la vérification des propriétés des fonctions (et pas de l’égalité syntaxique)

Question 2

Principe de la congruence closure

Answer 2

• On considère les termes qui apparaissent dans la conjonction et leurs sous-termes
• On cherche une partition maximale en classes d’équivalence telles que
  
  • Les égalités sont respectées : s ≈ t → s et t sont dans la même classe
  • La congruence est respecyée : (s_i)_i=1..n = (t_i)_i=1..n → f(s₁, …, s_n) et g(s₁, …, s_n) sont dans la même classe
• Le problème est insatisfiable s’il contient une inégalité s !≈ t telle que s et t sont dans la même classe

Question 3

Algorithme de congruence-closure

Answer 3

• Pour chaque terme t :
  
  • class(t) := {t}
• Pour chaque égalité s_i ≈ t_i :
  
  • class(s_i) := class(t_i) := class(s_i) ∪ class(t_i)
• Tant qu’il existe f(s₁, …, s_n) et f(t₁, …, t_n) tel que (s_i)_i=1..n = (t_i)_i=1..n et class(f(s)) != class(f(t))
  
  • class(f(s)) := class(f(t)) := class(f(s)) ∪ class(f(t))
• S’il existe s !≈ t tel que class(s) = class(t)
  
  • Retourner UNSAT
• Retourner SAT

Question 4

Complexité de l’implémentation de l’algorithme de congruence-closure par Nelson et Oppen

Answer 4

Complexité quadratique

Question 5

Comment raisonner avec l’égalité en logique propositionnelle (plutôt au premier ordre mais avec toutes les variables existentiellement quantifiées) ?

Answer 5

Avec l’algorithme de congruence-closure

Question 6

Comment raisonner avec l’égalité au premier ordre ?

Answer 6

En faisant de la saturation avec des règles d’inférence dédiées à l’égalité : superposition

Question 7

Quelles hypothèse simplificatrice fait-on pour appliquer la superposition ?

Answer 7

On considère que le seul prédicat des formules est l’égalité

Question 8

Comment supprimer tous les prédicats (à part l’égalité) d’une formule ?

Answer 8

Pour chaque prédicat p, le remplacer par un symbole de fonction f_p de même arité et ajouter à la signature un constante ⊤ de façon à ce qu’on puisse remplacer “p(t₁, …, t_n)” par “f_p(t₁, …, t_n) ≈ ⊤”

Question 9

Axiomes de la théorie de l’égalité

Answer 9

• Réflexivité
• Symétrie
• Transitivié
• Monotonicité pour chaque symbole de fonction f
• Monotonicité pour chaque symbole de prédicat p

Question 10

Règle de paramodulation

Answer 10

s ≈ t ∨ C₁ C₂[s’]
_________________
σ(C₁ ∨ C₂[t])
où σ est un mgu de s et s’ et s ≈ t équivaut à t ≈ s

Question 11

Règle de résolution d’égalité (pour la paramodulation)

Answer 11

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

Question 12

Quelles sont les propriétés qu’un ordre sur les termes doit respecter

Answer 12

• L’ordre doit être bien fondé
• L’ordre doit être compatible avec l’instanciation : pour tout σ, s, t, si s > t alors σ(s) > σ(t)
• L’ordre doit être total sur les termes sans variable

Question 13

Principe de la superposition

Answer 13

• Ordonner les termes avec un ordre qui respecte les bonnes propriétés
• Appliquer la règle de superposition, qui est similaire à la règle de paramodulation sauf qu’elle ne s’applique que lorsque on ne créée pas de terme plus grand

Question 14

Règle de superposition positive

Answer 14

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 15

Règle de superposition négative

Answer 15

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 16

Règle de résolution d’égalité (pour la superposition)

Answer 16

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

Question 17

Algorithme de saturation

Answer 17

• Appliquer l’algorithme de résolution en gérant l’ensemble des clauses à traiter comme un file
• Utiliser la congruence-closure pour détecter les tautologies

Question 18

Règle de factorisation d’égalité

Answer 18

s ≈ t ∨ s’ ≈ u ∨ C
____________________
σ(s ≈ t ∨ t !≈ u ∨ C)
où σ est un mgu de s et s’, σ(s) !≤ σ(t), σ(s) !≤ σ(u)