Алгоритм разрешения суждений с помощью КНФ.

 

Конъюнктивно-нормальной формой (КНФ) формулы называется такая формула, которая представляет собой конъюнкцию элементарных дизъюнкций. Элементарная дизъюнкция является тождественно-истинной, если она содержит хотя бы одну переменную со знаком отрицания и без него (а \/ в \/ а).

Чтобы определить, является ли некоторая формула тождественно-истинной, достаточно привести ее к КНФ.

1. Формализовать текст.

2. Привести формулу к нормальной форме.

3. При помощи равносильности «8» сделать конъюнкцию внешним знаком формулы.

Пример.

_ _

((а → в) ≡ (в → а))

1. При помощи формулы «21» и «14» избавиться от знаков эквиваленции и импликации.

____ = _ _ = _

((а \/ в) \/ (в \/ а)) /\ ((а \/ в) \/ (в \/ а))

2. С помощью формулы «2» и «12» избавиться от двойного отрицания:

_ _ _ _ _ _ _ _

((а /\ в) \/ (в \/ а)) /\ ((а \/ в) \/ (в /\ а)) ≡ ((а /\ в) \/ в \/ а) /\ ((а \/ в \/ (в /\ а))

 

3. При помощи равносильности «8» представить формулу в виде конъюнкции элементарных дизъюнкций

_ _ _ _ _ _

(а \/ в \/ а) /\ (в \/ в \/ а) /\ (а \/ в \/ в) /\ (а \/ в \/ а)

 

Вывод: каждый конъюнкт КНФ содержит переменную и ее отрицание. Следовательно, формула тождественно-истинна, является логическим законом.