Формулы. Алгоритм приведения формул к ДНФ (КНФ)
Формулу G назовем логическим следствием формул F1,…,Fn если при любой I при которой F1,…,Fn истинны, G также является
истиной.
Теорема: формула G является логическим следствием формул F1,…,Fn<*>F1<*>…<*>Fn->G - тождественно истинно.
Теорема: формула G является логическим следствием формул F1,…,Fn<*>F1<*>…<*>Fn<*>- тождественно ложно.
Формальное доказательство:
G – логическое следствие F1,…,Fn<*>
F1<*>…<*>Fn->G -экв- И<*>
-экв- Л<*> -экв- Л<*>
F1<*>…<*>Fn<*> -экв- Л.
Итак, доказательство того, что а является логическим следствием F1, F2, F3,…,Fn можно провести следующими способами:
1. Построить и сравнить таблицы истинности для F1<*>F2<*>F3<*>…<*>Fn и G .
2. Построить таблицы истинности для F1<*>F2<*>F3<*>…<*>Fn ->G и F1<*>F2<*>F3<*>…<*>Fn
3. Преобразовать выше указанную форму к ДНФ или КНФ.
Литерой назовём переменную и отрицание переменной.
Формулу, состоящую только из конъюнкций литер, назовём элементарной конъюнкцией.
Формулу, состоящую только из дизъюнкций литер, назовём элементарной дизъюнкцией.
ДНФ назовём формулу, состоящую из дизъюнкций элементарных конъюнкций.
КНФ назовём формулу, состоящую из конъюнкций элементарных дизъюнкций.
Алгоритм приведения формул к ДНФ (КНФ):
шаг 1: избавиться от -> и <->
шаг 2: перевести отрицание к переменным, избавиться от двойного отрицания
шаг 3: используя дистрибутивность (и другие законы), получить КНФ (ДНФ)
F -дизъ- (G<*>H) -экв- (F -дизъ- G)<*>(F -дизъ- H) – для получения КНФ
F<*>(H -дизъ- G) -экв- (F<*>G) -дизъ- (F<*>H) – для получения ДНФ.
ДНФ называется СДНФ, если элементарные конъюнкции, составляющие эту ДНФ, содержат все переменные или их отрицание и только
один раз.
КНФ называется СКНФ, если элементарные дизъюнкции, составляющие КНФ, содержат все переменные или их отрицание и только один
раз.
СКНФ дает тождественно истинную формулу <-> когда в каждой элементарной дизъюнкции содержится какая-либо переменная с
отрицанием.
СДНФ дает тождественную ложь <-> когда в каждой элементарной конъюнкции содержится какая-либо переменная с ее отрицанием.