Důkaz pravdivosti formule

Chceme-li dokázat logickou pravdivost formule v predikátové logice, pak budeme postupovat obdobně jako ve výrokové logice:

1. Formuli znegujeme
2. Formuli převedeme do klausulárního tvaru
3. Na formuli budeme postupně uplatňovat resoluční pravidlo. Pokud získáme prázdnou klausuli, je důkaz úspěšně ukončen.

Jinými slovy můžeme tedy říci, že formule je splnitelná právě když množina obsahuje prázdnou klausuli. Tento třetí bod však v predikátové logice nelze provést tak jednoduše jako ve výrokové logice. Problémem je to, že literály s opačným znaménkem, které bychom mohli při uplatňování rezoluce ”vyškrtávat”, mohou obsahovat různé termy.

Úloha: Uvažujme formuli v klausulárním tvaru: . Dokažte, že tato formule je nesplnitelná.

Řešení: Vypišme jednotlivé klausule pod sebe a pokusme se uplatňovat pravidlo rezoluce:

Klausule 1. a 3.obsahují literály s opačným znaménkem, avšak uplatnění rezoluce brání to, že . Uvědomme si však, že všechny proměnné jsou univerzálně kvantifikovány a že platí zákon konkretizace. Je-li tedy term t substituovatelný za ve formuli , pak , (znamená to tedy, že ”co platí pro všechny, platí i pro ”). Můžeme se pokusit najít vhodnou substituci termů za proměnné tak, abychom dostali shodné ”unifikované” literály. V našem příkladě taková substituce existuje: .

Po provedení této substituce dostaneme klausule:

1’.

2.

3‘.

kde na 1‘ a 3‘ již lze uplatnit pravidlo rezoluce:

4.

Abychom nyní mohli rezolvovat klausule 2. a 4., zvolíme opět substituci: .

Dostaneme

2‘.

4’.

a jejich rezolucí již obdržíme prázdnou klausuli. Tedy formule je nesplnitelná.

Úloha: Dokážeme správnost úsudku (analytickou pravdivost věty): „Jistý filosof odporuje všem filosofům, tedy odporuje sám sobě.“
Řešení: Interpretace bude nad množinou individuí, (podmnožina filosofů), (relace, ve které budou ty dvojice, kde první odporuje druhému) a větu tak analyzujeme jako .
Formuli znegujeme a převedeme na klausulární tvar: .

Vypišme jednotlivé klausule pod sebe a pokusme se uplatňovat pravidlo rezoluce:

1.

2.  

3.

Provedeme substituci {y/x}:

4.      z 1. a 2.

5.  □              z 3. a 4.

Obdrželi jsme prázdnou klausuli, původní úsudek je tedy pravdivý.