Алгоритм Куайна

Алгоритм Куайна, или алгоритм частичного перебора, позволяет доказать общезначимость формулы без просмотра полного семантического дерева. Основная идея алгоритма заключается в следующем: если при всех возможных расширениях некоторой частичной интерпретации формула А принимает одно и то же истинностное значение, то бесполезно строить поддерево, исходящее из узла, соответствующего этой частичной интерпретации. Рассмотрим работу алгоритма на примере.

Пример.Проверить общезначимость формулы(((pÙq)Ér)Ù (pÉq))É(pÉr).

1. Упорядочим множества элементов высказываний: {p, q, r}. Это эквивалентно тому, что дуги уровня 1 помечены литерой р, уровня 2 – литерой q, а уровня 3 – литерой r.

2. Рассмотрим те интерпретации, при которых р есть Т. При этом исходная формула сводится к формуле ((qÉr) Ùq) Ér.

3. Далее q интерпретируем как Т, тогда формула принимает вид r Ér – общезначимая формула.

4. Далее q интерпретируем как F, тогда формула принимает вид FÉr – тоже общезначимая формула, поэтому дальше строить поддерево не нужно.

5. Далее, рассмотрим те интерпретации, при которых p принимает значение F, тогда исходная формула имеет вид (FÉr) ÙT) ÉT – общезначимая формула. Следовательно, исходная формула всегда принимает значение Т, т.е. является общезначимой.

Этому примеру соответствует построение части семантического дерева, показанной на рисунке.