Специальные формы КНФ — различия между версиями
Rybak (обсуждение | вклад) (→КНФ в форме Хорна) |
Rybak (обсуждение | вклад) |
||
Строка 1: | Строка 1: | ||
− | Рассмотрим две формы, с помощью которых можно представить формулы, заданные в [[Определение булевой функции#Представление булевых функций|конъюнктивной нормальной форме]], то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов | + | Рассмотрим две формы, с помощью которых можно представить формулы, заданные в [[Определение булевой функции#Представление булевых функций|конъюнктивной нормальной форме]], то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов. |
− | = КНФ в форме Крома = | + | == КНФ в форме Крома == |
{{Определение | {{Определение | ||
|definition= | |definition= | ||
− | '''Конъюнктивная нормальная форма(КНФ) в форме Крома''' - это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких литералов, количество которых не превышает двух.}} | + | '''Конъюнктивная нормальная форма(КНФ) в форме Крома''' {{---}} это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких литералов, количество которых не превышает двух.}} |
'''Пример :''' | '''Пример :''' | ||
Строка 13: | Строка 13: | ||
*Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Крома можно удовлетворить(т.е КНФ в форме Крома не является тождественным <tex>0</tex>). | *Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Крома можно удовлетворить(т.е КНФ в форме Крома не является тождественным <tex>0</tex>). | ||
− | |||
*Функцию <tex>F</tex> можно задать в форме Крома <tex> \iff </tex> выполнено следующее следствие: | *Функцию <tex>F</tex> можно задать в форме Крома <tex> \iff </tex> выполнено следующее следствие: | ||
Строка 23: | Строка 22: | ||
{{Определение | {{Определение | ||
|definition= | |definition= | ||
− | '''Конъюнктивная нормальная форма(КНФ) в форме Хорна''' - это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания.}} | + | '''Конъюнктивная нормальная форма(КНФ) в форме Хорна''' {{---}} это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания.}} |
'''Пример:''' | '''Пример:''' |
Версия 00:31, 15 октября 2011
Рассмотрим две формы, с помощью которых можно представить формулы, заданные в конъюнктивной нормальной форме, то есть имеющей вид конъюнкции выражений в скобках, каждое из которых представляет собой дизъюнкцию одного или нескольких литералов.
КНФ в форме Крома
Определение: |
Конъюнктивная нормальная форма(КНФ) в форме Крома — это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию нескольких литералов, количество которых не превышает двух. |
Пример :
Утверждения:
- Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Крома можно удовлетворить(т.е КНФ в форме Крома не является тождественным ).
- Функцию можно задать в форме Крома выполнено следующее следствие:
КНФ в форме Хорна
Определение: |
Конъюнктивная нормальная форма(КНФ) в форме Хорна — это конъюнкция выражений в скобках, каждое из которых представляет собой дизъюнкцию литералов, в которой присутствует не более одного литерала без отрицания. |
Пример:
Каждая скобка представляет собой Дизъюнкт Хорна.
Любую формулу можно представить в виде КНФ в форме Хорна. Для этого формулу необходимо преобразовать в конъюнкцию элементарных дизъюнкций и далее каждую дизъюнкцию представить в форме дизьюнкта Хорна.
Утверждения:
- Существует алгоритм, который за полиномиальное время проверяет, что функцию, заданную в форме Хорна можно удовлетворить.
- Функцию можно задать в форме Хорна выполнено следующее следствие: