Формы представления формул логики высказываний

КНФ также называют клаузальной формой.

Клауза – элементарная дизъюнкция.

Литера, литерал – элементарное высказывание или его отрицание.

Дизъюнкт – дизъюнкция конечного числа литералов.

Хорновский дизъюнкт имеет не более одной не инверсной литеры.

Пример.

.

Хорновские дизъюнкты используются в языке ПРОЛОГ (PROLOG, от PROgramming in LOGic – программирование в логике; разработан в 1972 г. Аланом Колмари) для описания правил типа «Если, то». Кстати, в ПРОЛОГЕ с помощью импликации записываются и так называемые факты: .

.

Т.е. факт – это утверждение истинности некой формулы.

Преобразование в КНФ обычно производится при помощи распределительного закона.

СКНФ получают из КНФ путём добавления к каждому дизъюнкту тождественно ложной литеры.