Методы и алгоритмы проверки выводимости

Определение 2. Пусть задана совокупность ППФ , которая называется посылками (иногда гипотезами), и ППФ – . « » называется логическим следствием . или выводимой из А (записывается как ⊦ ), если является тавтологией (тождественно истинным высказыванием).

Таким образом, задача проверки выводимости сводится к проверке на тождественную истинность. Существует несколько десятков методов и алгоритмов установления тождественной истинности логической формулы.

1. Алгоритм истинностных таблиц (АИТ) для F=A®B.

АИТ сводится к последовательной подстановке всех возможных интерпретаций (наборов «истина» и «ложь») переменных, входящих в . Алгоритм останавливается, если значение ложь ( не выполнима, а значит не выводима из на всех интерпретациях); истина ( выполнима на всех интерпретациях, значит суть тавтология и А⊦ . Такой алгоритм требует в наихудшем случае 2ⁿ подстановок (2ⁿ возможных интерпретаций), где «n» число переменных, входящих в формулу F.

2. Алгоритм Квайна(Квайн. 1960 г. США)

Идея: при последовательных подстановках значений переменных можно уменьшить длину формулы, исходя из совокупности проведённых проверок истинности F, и тем самым сокращать число переменных для проверки.

Вводится понятие дерева испытаний, которое по сути дела представляет собой граф всех интерпретаций проверяемой формулы . Квайн назвал его «семантическим деревом».

Пример 3. Построение семантического дерева.

Пусть необходимо проверить общезначимость формулы

Семантическое дерево. Каждое левое ребро дерева соответствует переменным , а каждое правое ребро – .

Каждая ветвь (например, самая левая) соответствует набору (p×q×r), самая правая . Дерево перечисляет все возможные элементарные конъюнкции.

1)

Положим для F (вершина ) , тогда

(напомним, что –

(формула в вершине «1»)

2) Положим для , тогда

.

(формула в вершине «2»)

3)

Спустимся до вершины . Положим для , тогда значение (формула в вершине «3»).

4) Поднимемся к вершине , в положим , тогда (формула в вершине «4»).

Поднимемся к вершине и в положим , следуя нумерации вершин, находим, что . . Можно заметить характерное правило обхода вершин.

Такой алгоритм обхода вершин семантического дерева называется алгоритмом с возвратом (back tracking). На рисунке показан путь обхода семантического дерева. В процессе обхода вычисляется значение формулы F. Оказывается, что на всех наборах значений . Таким образом F является тавтологией.

3. Метод резолюций (Д.Робинсон, 1965 г., США).

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

Множество дизъюнктов S не выполнимо тогда и только тогда, когда логическое следствие из него есть пустой дизъюнкт, т. е. дизъюнкт, всегда принимающий значение F. Таким образом, невыполнимость множества дизъюнктов S можно проверить, порождая логические следствия из него до тех пор, пока не получится пустой дизъюнкт.

Алгоритмы доказательства выводимости А⊦B, построенные на основе этого метода, применяются во многих системах искусственного интеллекта, а также являются фундаментом, на котором построен язык логического программирования «Пролог».

Метод резолюций использует несколько принципов.

Сведение к противоречию.

Пусть правильно построенное рассуждение с элементарными высказываниями .

Тогда , отсюда и .

2) Представление формул для и в виде КНФ

, где Д и Д^’ – дизъюнкты.

3) Правило резолюций R для обработки совмещенного списка дизъюнктов.

Объединенный Д₁= С₁Ú х_i

список Д₂= С₂Ú х_i

дизъюнктов Д, …………. · С₁Ú С_j

входящих ….……… ·

в P и Д_j = С_j Ú х_i

…………. Оставшийся

Д_m₊_n список

дизъюнктов

а) Каждый дизъюнкт из Д представим в виде , где «С» все остальные переменные, входящие в дизъюнкт, x_i выделенная переменная с отрицанием , либо без отрицания . Из списка выделяется пара, как показано на рисунке, с общей переменной x_i с отрицанием и без него.

б) По правилу резолюции (закону резолюции), который является тавтологией (доказательство этого факта можно сделать)

пара дизъюнктов редуцировалась в дизъюнкт ⊦ .

в) Образуется новый список дизъюнктов из дизъюнктов. (оставшийся список дизъюнктов). Такой список называется редуцированным. Очевидно, что размерность редуцированного списка по сравнению с исходным уменьшилась на «1».

г) далее правило R применяют к редуцированному списку дизъюнктов.

д) Останов наступает, когда в списке остаются только два дизъюнкта вида и , либо применение R невозможно.

Список дизъюнктов редуцировался в КНФ

В этом случае говорят, что S логически следует из Р или S выводимо из Р.

123

Не нашли, что искали? Воспользуйтесь поиском по сайту: