Splnitelnost a platnost formule

Všechny atomické formule obsahující pouze prvotní proměnné jsou evidentně splnitelné. Atomická formule tvořena logickou konstantou true je tautologie, zatímco false je kontradikce neboli nesplnitelná atomická formule.

Kontradikce jsou nesplnitelné neboli nekonsistentní formule.

Platné formule jsou zároveň formulemi splnitelnými neboli konsistentními.

Platnost a nesplnitelnost jsou duální pojmy. Formule A je platná, právě tehdy když formule A je nesplnitelná.

Vztah mezi pojmy splnitelnosti a platnosti formule znázorňuje následující obrázek.

Při rozhodování platnosti nebo splnitelnosti formule A často hovoříme o rozhodovacích algoritmech (rozhodovací procedura, která úspěšně provede a skončí odpovědí ANO, patří-li A do množiny platných (splnitelných) formulí, resp. skončí odpovědí NE, jestliže A do této množiny nepatří.

Algoritmy rozhodování splnitelnosti a platnosti formulí

Problém spočívá pouze ve složitosti tohoto rozhodování. Jedním z dosud nevyřešených problémů informatiky je otázka, zda-li existuje rozhodovací procedura splnitelnosti formule.

Rozhodování pomocí sémantického stromu

Vzhledem k tomu, že formuli obsahující k symbolů označující atomické výroky p₁, ..., p_k  lze interpretovat 2^p způsoby, je třeba uvažovat o efektivnějších procedurách, než je např. u pravdivostních tabulek zkoušení všech variant ohodnocení proměnných atomických formulí.

Řada rozhodovacích algoritmů je založena na pojmu sémantický strom. Každá proměnná p výrokové formule je v něm zastoupena dvojicí literálů, tj. pozitivním literálem proměnné p zastupujícím jeho pravdivostní hodnotu true a negativním literálem p zastupující jeho pravdivostní hodnotu false. Strom složený z hran a uzlů tvoří systém větví procházejících uzly vždy od kořene až po list.

Úplný sémantický stroj zachycuje v případě konečné formule všechna možná ohodnocení jejich proměnných.

Formule je splnitelná (konsistentní), jestliže alespoň jeden list odpovídajícího sémantického stromu nese výslednou hodnotu interpretace true.

Formule je platná (tautologická), jestliže všechny listy jejího úplného sémantického stromu nesou výslednou hodnotu interpretace true.

Rozhodování pomocí tablové metody

Sémantický strom napomáhá přehlednému uspořádání možných ohodnocení atomů dané formule a umožňuje sledování pouze těch větví, kde pravdivostní hodnota koncového listu není určena již dříve během průchodu uvažovanou větví. Podobným nástrojem přehledné prezentace formule je i její formační strom, znázorňující syntax formule.

Jistou modifikací využití formačního stromu je tablová metoda znázornění postupného rozkladu formule až na její literály.

Vhodnou pomůckou pro vytváření sémantického tabla jsou pravidla přepisu formulí na konjunkce literálů vyskytujících se proměnných, které představují sekvence zavěšené na listech sémantického tabla.

-pravidla:

-pravidla:

Prakticky jsou postupy rozhodování platnosti, resp. splnitelnosti formule, popsané v tomto a předcházejícím odstavci uplatnitelné pouze pro nepříliš složité formule. Poněkud lépe je na tom rezoluční metoda.

Robinsonův rezoluční princip

Je-li množina klauzulí nesplnitelná, pak opakovaným užitím rezolučního pravidla lze vždy odvodit spor (prázdnou klauzuli), která je nesplnitelná.

Popsaný algoritmus zjišťování nesplnitelnosti je nedeterministický. Existuje více než jeden způsob postupného výběru dvojic klauzulí pro aplikaci rezolučního principu.

Rezoluční princip poskytuje možnost důkazu, že formule Z je (tauto)logickým důsledkem dané množiny formulí, tedy že platí H₁, H_2, ..., H_n |= Z. Důkaz tautologického důsledku lze totiž převést na důkaz nesplnitelnosti množiny formulí 

{H₁, H_2, ..., H_n, Z}.