Previous Contents Next

4   Résolution

Définition 10   Soit C une clause. C où toutes les variables sont remplacées par un terme clos est appelée instance close de C
Exemple : S={a0,f1}, C={p(x),q(x,y)} : {p(a),q(a,f(a))}

On peut alors appliquer la méthode de résolution (propositionnelle) à des instances closes.

Exemple : Montrer que On montre que H1 Ù H2 Ù ¬ C n'est pas satisfiable.

Forme prénexe :
$ z" x " y  (p(x) ® q(x)) Ù (q(y) ® r(y)) Ù p(z) Ù ¬ r(z)
Skolémisation (nouvelle constante c), forme clausale :
{p(x) ® q(x),q(y) ® r(y),p(c),¬ r(c)}
Instances closes (avec la signature minimale : S={c}) : Résolution : Un théorème de Herbrand nous assure qu'on peut se restreindre à cette signature minimale (l'ensemble des symboles fonctionnels qui apparaissent dans les clauses).

4.1   Unification

Définition 11   Une substitution s est une application de l'ensemble des variables V dans l'ensemble des termes. Une substitution peut être étendue à l'ensemble des termes et des atomes.
Exemple : S={a0,f1,...}, P={p1,...}. On définit s par
x |® a
y |® f(z)
alors
s(f(x)) = f(a)           terme
s(p(f(x))) = p(f(a))        atome
s(p(y)) = p(f(z))
On pourra noter s={x¬ a, y¬ f(z)}

Définition 12   Soit deux termes t1 et t2. On appelle unificateur de t1 et t2 une substitution s telle que s(t1)=s(t2) (t1 et t2 sont unifiables).

On appelle su l'unificateur le plus général, l'unificateur tel que pour tout unificateur s', pour tout terme t, s'(t) est une instance de s(t).
Intuition : su est l'unificateur qui « fait le minimum ».

Exemple : pour <f(x,a),f(y,z)> Algorithme d'unification de deux termes t1 et t2
  1. Initialisation : E:={<t1,t2>}, s:=Ø
  2. Tant que E¹Ø
    1. Soit E:=E\ <t,t'>
    2. Si t=t' alors continuer
    3. Si t=xÎ V (resp. pour t'=xÎ V)
      1. Si xÎ V(t') alors échec (test d'occurrence)
      2. Sinon, s := s ° {x¬ t'}, E := s (E)
    4. Sinon t=f(t1,...,tn), t'=f'(t'1,...,t'n')
      1. Si f¹ f' alors échec
      2. Sinon E:= EÈ{<ti,t'i>/ 1£ i£ n}
  3. s est l'unificateur le plus général (s'il n'y a pas eu échec)
Exemple : S={f3, a0, g1}, x,y,zÎ V
<f(a,g(x),x),f(y,g(y),z)>

4.2   Principe de résolution

Définition 13   Soient deux clauses C et C' telles que AÎ C, ¬ A'Î C' et A et A' sont unifiables par s le plus grand unificateur. R=s(C \ A È C'\¬ A') est la résolvante de C et C'.

Propriété 22   {C,C'} et {C,C',R} sont équivalents

Propriété 23   Soit E un ensemble de clauses. E est insatisfiable si et seulement si on peut obtenir la clause vide par application répétée du principe de résolution.
Exemple : Montrer que s(j) est déductible de
" x" y  (h(y) Ù i(x,y) Ù a(x) ® d(x))
" x (" y  (i(y,x) Ù b(y)) ® d(y)) ® s(x)
h(j)
" x (b(x) ® a(x))

Previous Contents Next