Tato stránka je věnována různým nekategorizovaným poznámkám k přednášce. Budou zde uveřejňovány například chyby nalezené ve slidech.

Přednáška 8
Několik poznámek k redukčnímu algoritmu
Předně je třeba poznamentat, že redukční algoritmus nahrazuje literály vstupní formule. To znamená, že literál tvaru ¬∀i∈T_I.φ_I(i)→φ_V(i) je nahrazován pomocí pravidla pro existenční kvantifikátor, tedy podformulí (φ_I(i)→φ_V(i))[i/j], kde j je nová proměnná. Literál tvaru ∀i∈T_I.φ_I(i)→φ_V(i) je nahrazován pomocí pravidla pro univerzální kvantifikátor, tedy konjunkcí podformulí (φ_I(i)→φ_V(i))[i/e], kde e je výraz, kterému se i může rovnat (jsou to výrazy ze stráží a výrazy použité jako indexy, přičemž se nejedná o kvantifikované proměnné, dále jen výrazy).

Dále je třeba oveřit, že pro formule ve tvaru NNF, kde atomy jsou podformule tvaru ∀i∈T_I.φ_I(i)→φ_V(i) (resp. obecněji pro více kvantifikovaných indexových proměnných), uvedené náhrady zachovávají splnitelnost (tj. výsledná formule je ekvivalentně splnitelná s původní). Platí, že pravdivostní hodnota formule φ(i)[i/j], kde j je nová proměnná, je při daném ohodnocení měnší nebo rovna pravdivostní hodnotě formule ∃i∈T_I.φ(i) při stejném ohodnocení. Je-li splnitelná formule po provedení náhrad existenčních kvantifikátorů, je díky monotonii formulí NNF a uvedené nerovnosti splnitelná i původní formule. Je-li splnitelná původní formule, jsou splněny některé její literály s existenčním kvantifikátorem. Potom stačí vzít ohodnocení nových proměnných pomocí hodnot dosvědčujících platnost splněných literálů s existenčními kvantifikátory. U nesplněných literálů stačí brát ohodnocení nových proměnných libovolné. Díky monotonii je výsledná formule opět splněna.

U náhrad univerzálních kvantifikátorů je třeba vzít v úvahu, že logika pro prvky dovoluje pouze rovnosti. Je-li splněna původní formule nějakým ohodnocením proměnných, je potom stejným ohodnocením splněna i formule po provedení náhrad. Je-li naopak splněna formule po provedení náhrad univerzálních kvantifikátorů nějakým ohodnocením, pak lze toto ohodnocení upravit tak, aby jím byla splněna původní formule. Úprava se bude týkat realizace polí. Prvky polí v upravené realizaci ohodnotíme stejně jako jsou ohodnoceny prvky odpovídajích polí v původní realizaci na pozici odpovídající nejbližšímu výrazu, který ohraničuje (shora nebo zdola) daný prvek pole. Pravdivostní hodnota podformule s kvantifikátorem bude pro volbu kvantifikované proměnné rovnu pozici daného prvku pole stejná jako pravdivostní hodnota této podformule pro volbu kvantifikované proměnné rovné nejbližšímu ohraničujícímu výrazu. Toto platí diky tomu, že použitá logika pro prvky dovoluje pouze rovnosti. Jestliže je splněna upravená formule v NNF tvaru, jsou jejím splňujícím ohodnocením splněny některé literály odpovídající konjunkcím vzniklým náhradou univerzálních kvantifikátorů. Ohodnocení vzniklé výše popsanou úpravou splní tytéž literály v původní formuli. Tedy původní formule bude rovněž splnitelná.