Rezoluční pravidlo a algoritmus unifikace v predikátové logice 1. řádu

Rezoluční metoda v predikátové logice je obdobou stejnojmenné metody ve výrokové logice, s tím rozdílem že je složitější. Může za to bohatější struktura predikátové logiky. Tato metoda se používá v logickém programování a je základem pro Prolog (programovací jazyk).

Při uplatňování rezoluční metody je nutné nejprve formuli převést do Skolemovy klauzulární formy.

 
Zavedení základních pojmů:

Literál - je atomická formule, nebo negace atomické formule. např.: P(x, g(y)), ¬Q(z)

Klauzule - je disjunkce literálů, např.:  P(x, g(y)) ∨ ¬Q(z)

Skolemova klauzulární forma - ∀x1…xn [C1 ∧ … ∧ Cm], uzavřená formule, kde Ci jsou klausule. Všechny kvantifikátory stojí na začátku formule a neobsahuje žádný existenční kvantifikátor.

Skolemizace - proces odstranění existenčních kvantifikátorů, je jedním z kroků převodu do skolemovy klauzulární formy

          ∃x ∀y1...yn A(x, y1,...,yn) ⇒ ∀y1...yn A(c, y1,...,yn) ,kde c je nová dosud nepoužitá konstanta

           ∀y1...yn ∃x A(x, y1,...,yn) ⇒ ∀y1...yn A(f(y1,...,yn), y1,...,yn) ,kde f je nový dosud nepoužitý funkční symbol

          ⇒  pokud je existenční kvantifikátor první - přepíšeme proměnnou (tu za kvantifikátorem) uvnitř formule za novou konstantu, pokud je existenční kvantifikátor druhý - přepíšeme proměnnou za funkci s atributem druhé proměnné, u obou případů smažeme při přepisu existenční kvantifikátor 

Příklad skolemizace:

∃y∀z P(z,y) ∧∀x∃u Q(x,u) ⇔ ∀z P(z,a) ∧∀x Q(x,f(x)) ⇔ ∀z∀x [P(z,a) ∧ Q(x,f(x))] 

Převod do Skolemovy klauzulární formy

Krok 1. a 7. nejsou ekvivalentní, pouze zachovávají splnitelnost formule. 

  1. Utvoření existenčního uzávěru (zachovává splnitelnost)
  2. Eliminace nadbytečných kvantifikátorů
  3. Eliminace spojek É, ≡
  4. Přesun negace dovnitř
  5. Přejmenování proměnných
  6. Přesun kvantifikátorů doprava
  7. Eliminace existenčních kvantifikátorů (Skolemizace – zachovává splnitelnost)
  8. Přesun všeobecných kvantifikátorů doleva
  9. Použití distributivních zákonů
Příklad převodu do Skolemovy klauzulární formy:

∀x {P(x) É ∃z {¬∀y [Q(x,y) É P(f(x1))] ∧ ∀y [Q(x,y) É P(x)]}}

1.,2. Existenční uzávěr a eliminace ∃z:

   ∃x1 ∀x {P(x) É {¬∀y [Q(x,y) É P(f(x1))] ∧ ∀y [Q(x,y) É P(x)]}}

3.,4. Přejmenování y, eliminace É:

   ∃x1 ∀x {¬P(x) ∨ {¬∀y [¬Q(x,y) ∨ P(f(x1))] ∧ ∀z [¬Q(x,z) ∨ P(x)]}}

5.,6. Negace dovnitř a kvantifikátory doprava:

   ∃x1 ∀x {¬P(x) ∨ {[∃y Q(x,y) ∧ ¬P(f(x1))] ∧ [∀z ¬Q(x,z) ∨ P(x)]}}

7. Eliminace existenčních kvantifikátorů:

   ∀x {¬P(x) ∨ {[Q(x,g(x)) ∧ ¬P(f(a))] ∧ [∀z ¬Q(x,z) ∨ P(x)]}}

8. Kvantifikátor doleva:

   ∀x ∀z {¬P(x) ∨ {[Q(x,g(x)) ∧ ¬P(f(a))] ∧ [¬Q(x,z) ∨ P(x)]}}

9. Distributivní zákon:

   ∀x ∀z {[¬P(x) ∨ Q(x,g(x))] ∧ [¬P(x) ∨ ¬P(f(a))] ∧ [¬P(x) ∨  ¬Q(x,z) ∨ P(x)]}

10. zjednodušení:

   ∀x {[¬P(x) ∨ Q(x,g(x))] ∧ [¬P(x) ∨ ¬P(f(a))]}

 

Unifikace literálů

Chceme-li rezolvovat klauzule, brání nám to, že termy / argumenty nejsou stejné. Všechny proměnné jsou ale kvantifikovány všeobecným kvantifikátorem, a tudíž můžeme použít zákon konkretizace a pokusit se najít vhodnou substituci termů za proměnné tak, abychom dostali shodné ”unifikované” literály.

Zákon konkretizace:  Je-li term t substituovatelný za x ve formuli  A(x), pak ∀x A(x) |= A(x/t)

Příklad:
  1. P(x, f(x))
  2. ¬P(a, z) ∨ ¬Q(z, v)  
  3. Q(y, h(y))


⇒ provedeme substituci     

     x/a, z / f(a)
  1. P(a,f(a))
  2. ¬P(a, f(a)) ∨ ¬Q(f(a), v) 
  3. Q(a, h(a))  

 

Pro automatickou unifikaci se používají 2 algoritmy:

  • Herbrandova procedura
  • Robinsonův unifikační algoritmus 

 

Postup důkazů rezoluční metodou

  • Důkaz, že formule A je logicky pravdivá 
    1. Formuli A znegujeme
    2. ¬A převedeme do Skolemovy klausulární formy
    3. Uplatňujeme pravidla rezoluce a dokazujeme splnitelnost formule
  • Důkaz platnosti úsudku P1,...Pn |- Z
    1. Závěr znegujeme
    2. Formule P1,...Pn a ¬Z převedeme do klausulární formy
    3. Uplatňujeme pravidla rezoluce a dokazujeme nesplnitelnost formule
Příklad rezoluční metody v PL1:

∀x∀y [{P(x,y) É Q(x, f(g(x)))} ∧ {R(x) ∨ ∃x ¬Q(x, f(g(x)))} ∧ ∃x ¬R(x)] É ∃x ¬P(x, g(x))

1)  Formuli znegujeme:

∀x∀y [{P(x,y) É Q(x, f(g(x)))} ∧ {R(x) ∨ ∃x ¬Q(x, f(g(x)))} ∧ ∃x ¬R(x)] ∧ ∀x P(x, g(x))

2)  Odstraníme existenční kvantifikátory a přejmenujeme:

∀x∀y [{P(x,y) É Q(x, f(g(x)))} ∧ {R(x) ∨ ¬Q(a, f(g(a)))} ∧ ¬R(b)] ∧ ∀z P(z, g(z))

3)  Odstraníme implikace:

∀x∀y [{¬P(x,y) ∨ Q(x, f(g(x)))} ∧ {R(x) ∨ ¬Q(a, f(g(a)))} ∧ ¬R(b)] ∧ ∀z P(z, g(z)) 

4)  Sepíšeme pod sebe a uplatňujeme pravidla rezoluce a unifikace literálů:

  1.  ¬P(x,y) ∨ Q(x, f(g(x)))
  2.  R(x) ∨ ¬Q(a, f(g(a)))
  3.  ¬R(b)
  4.  P(z, g(z)                                                     
  5.  Q(x, f(g(x)))         1,4:     z/x,   y/g(x)
  6.  ¬Q(a, f(g(a)))       2,3:     x/b
  7. ▢

⇒ vyšla prázdná klauzule, z čehož plyne že negovaná formule je nesplnitelná (kontradikce), proto je původní formule logicky pravdivá

 

 Čerpáno ze skript Logika pro Informatiky (Doc. RNDr. Marie Duží)