Логика булевых функций

3.4. Автоматическое доказательство теорем. Метод резолюций.

Пусть имеется множество формул Г = {A₁, A₂, …, A_n} и формула B. Автоматическим доказательством теоремы B называют алгоритм, который проверяет вывод

A₁, A₂, …, A_n ├ B. (3. 1)
Выражение (3.1) можно прочитать следующим образом:
Если посылки A₁, A₂, …, A_nистинны, то истинно заключение B.
или
Если причины A₁, A₂, …, A_nимели место, то будет иметь место следствие B.
Проблема доказательства в логике состоит в том, чтобы установить, что если истинны формулы A₁, A₂, …, A_n, то истинна формула B.
В общем случае такой алгоритм построить нельзя. Но для некоторых частных случаев такие алгоритмы существуют. Доказательство теоремы равносильно доказательству общезначимости некоторой формулы. Наиболее эффективно доказательство общезначимости формул осуществляется методом резолюций. Процедура поиска доказательства методом резолюций фактически является процедурой поиска опровержения, т. е. вместо доказательства общезначимости формулы доказывается, что отрицание формулы противоречиво:
A  И  A  Л.
Введем терминологию, обычно употребляемую при изложении метода резолюций.
Литерой будем называть выражения A или A. Литеры A и A называются контрарными, а множество {A, A} – контрарной парой.
Дизъюнкт – это дизъюнкция литер (или элементарная дизъюнкция).
Пример 3.6.
A  B  C – дизъюнкт;
A  B – дизъюнкт;
A  B & C – не дизъюнкт;
A – дизъюнкт.
Дизъюнкт называется пустым, (обозначается ), если он не содержит литер. Пустой дизъюнкт всегда ложен, так как в нем нет литер, которые могли бы быть истинными при любых наборах переменных.
Рассмотрим применение метода резолюций к исчислению высказываний.
Правилом резолюции называют следующее правило вывода:
. (3. 2)
Правило (3.2) можно также записать в следующем виде:
AB, AC ├ B  C. (3. 3)
Правило резолюций можно доказать, используя равносильности логики высказываний:
(AB) & (AC)  (B  C) = ((AB) & (AC))  (B  C) = (AB)  (AC)  (B  C) = A&B  A&C  (B  C) = (A A) & (A C) & (B A) & (B C)  (B  C) = (A C) & (B A) & (B C)  (B  C) =(A C  B  C) & (B A  B  C) & (B C  B  C) = И.
Итак, при истинных посылках истинно заключение.
Правило (3.2) – единственное правило, применяемое в методе резолюций, что позволяет не запоминать многочисленных аксиом и правил вывода.
Дизъюнкт BC называется резольвентой дизъюнктов AB и AC по литере A:
BC = res_A(AB и AC).
Если дизъюнкты не содержат контрарных литер, то резольвенты у них не существует.
Для дизъюнктов A и A резольвента есть пустой дизъюнкт: res_A(A, A) = .
Пример 3.7.
Пусть F = A  B  C, G = A  B  D.
Тогда
res_A(F, G) = B  C  B  D.