Obecná rezoluční metoda a logické programování

Rezoluční metoda je metodou pro ověřování tautologií a logického vyplývání. Můžeme ji provádět buď ve výrokové logice nebo v predikátové logice. Pro osvěžení základních znalostí z logiky si můžeš pročíst kapitolu o matematické logice.

Rezoluční metoda je univerzální dokazovací metodou, kterou lze využít pro automatické strojové zpracování formulí a je základem pro logické programování (prolog). Pomocí rezoluční metody můžeme dokazovat, že formule je nesplnitelná (důkaz sporem). U výrokové logiky můžeme použít i přímý důkaz, a určit co vyplývá z daných předpokladů (odvození rezolventa).

Rezoluční metoda ve výrokové logice

Touto metodou dokazujeme nesplnitelnost dané formule (resp. množiny formulí) a je uplatnitelná na formuli v konjunktivní normální formě (KNF). Využívá dvou jednoduchých tvrzení:

1)  Je-li formule A tautologie, pak formule ¬A je kontradikce a naopak. 

     |= A právě když ¬A |=

2)  Rezoluční pravidlo odvozování: Nechť p je literál. Z formule (A ∨ p) ∧ (B ∨ ¬p) odvodíme (A ∨ B). Zapisujeme:

      (A ∨ p) ∧ (B ∨ ¬p)

      –––––––––––––––

             (A ∨ B)

     Toto pravidlo není přechodem k ekvivalentní formuli, ale zachovává splnitelnost. 

Příklad:

Je doma nebo odešel do kavárny.

Je-li doma, pak nás očekává.

-------------------------------------------------------

Z: Jestliže nás neočekává, pak odešel do kavárny.

      

 d ∨ k

 d É o  ⇔  ¬d ∨ o

 –––––––––––––––––––

 ¬o É k  ⇔  o ∨ k

 

Splnitelnost formule můžeme ověřit buď přímo nebo nepřímo - sporem.

(1) Přímý důkaz:

- Jednotlivé klausule napíšeme pod sebe a odvozujeme rezolventy (které vyplývají).

  1.   d ∨ k
  2.   ¬d ∨ o
    –––––––––––––––
  3.   o ∨ k      (1. a 2.)

 ⇒ z 1. a 2. formule jsme odvodili 3. řádek a zjistili jsme že se shoduje se závěrem příkladu. Úsudek je tudíž platný. 

 

(2) Nepřímý důkaz sporem:

Při nepřímém se snažíme dojít k prazdné klauzuli. Při ověřování splnitelnosti negujeme závěr formule a snažíme se dojít ke sporu (prázdné klauzuli).

  1.   d ∨ k
  2.   d ∨ o
  3.   ¬o           ... negovaný závěr
  4.   ¬k           ... negovaný závěr
    –––––––––––––––
  5.   d      (1. a 4.)
  6.   o      (2. a 5.)
  7.   ▢      (3. a 6.)

 ⇒ v 7. kroku jsme dostali prázdnou klauzuli. Negovaný závěr je tudíž ve sporu s předpoklady, a proto je úsudek platný.