Převod formule do prenexního normální tvar (a jádra do CNF či DNF)

Každou formuli predikátové logiky 1. řádu lze převést na formuli v tzv. prenexním normálním tvaru, která je původní formuli ekvivalentní. Formule v tomto tvaru začíná kvantifikátory (obecné a existenční), které kvantifikují za nimi následující jádro. Jádro je otevřená formule, tj. formule, která neobsahuje kvantifikované proměnné. Pro převod formule do prenexního tvaru existuje několik málo pravidel, které formuli rekurzivně převádějí.

Přehled prenexních pravidel

Prenexní pravidla

Jádro lze dále převést do konjunktivního, resp. disjunktivního normálního tvaru (CNF, resp. DNF). Formule v CNF (DNF) je stručně řečeno konjunkce disjunkcí (disjunkce konjunkcí). Opět s pomocí několika jednoduchých pravidel lze ve třech krocích každou otevřenou formuli do normálního tvaru převést.

Přehled pravidel převodu do CNF a DNF

Pravidla převodu do CNF a DNF

Výše uvedené převody formulí byly předmětem mé zápočtové práce z předmětu Neprocedurálního programování. Jde o program v Prologu, který ke svému spuštění vyžaduje nainstalovaný interpret SWI-Prolog, který je dostupný pro všechny rozšířené platformy.