Автоматическое доказательство теорем. Тема 5

1.

АВТОМАТИЧЕСКОЕ
ДОКАЗАТЕЛЬСТВО ТЕОРЕМ
ТЕМА 5

2.

В предыдущих лекциях мы уже говорили, что
не существует универсального эффективного
алгоритма, позволяющего для любой формулы
определять, является ли она теоремой
(тавтологией) ИП или нет. Тем не менее есть
алгоритмы, которые подтверждают
тождественную истинность общезначимых
формул, а для остальных формул не
останавливаются в общем случае.
Большинство подобных алгоритмов основаны
на алгоритме Эрбрана, который мы
рассмотрим в данной лекции.

3.

Если рассмотреть бескванторную формулу Ф и
заменить все атомарные формулы
предметными переменными (разные формулы
на разные переменные, одинаковые – на
одинаковые переменные), то получится
формула логики высказываний, которую
принято называть прототипом формулы Ф.
Теорема 1. Бескванторная формула
общезначима в том и только в том случае, если
ее прототип – тавтология ИВ.
Доказательство. Если прототип формулы Ф
является тавтологией, то формула Ф является
частным случаем пропозициональной
тавтологии, значит, выводима и общезначима.

4.

ТЕОРЕМА 2 (ТЕОРЕМА ЭРБРАНА)
Пусть
, где Ф –
бескванторная формула. Формула Ψ
общезначима в том и только в том случае, если
для некоторого конечного набора термов
,
для
будет общезначима дизъюнкция
формул
.
Пример. Рассмотрим формулу
,
где a,b – константы.
Подставим в формулу x=a и x=b, запишем
дизъюнкцию
. Эта
формула - тавтология, так как при любом
значении P(a,b) данная дизъюнкция истинна.
Здесь n = 2.

5.

ТЕОРЕМА 3 (ТЕОРЕМА ЭРБРАНА)
Пусть
, где Ф –
бескванторная формула. Формула Ψ
невыполнима в том и только в том случае, если
для некоторого конечного набора термов
,
для
будет невыполнима конъюнкция
формул
.
Из теоремы 1 следует, что эта конъюнкция
невыполнима в том и только в том случае, если
ее прототип – противоречие ИВ.

6.

МЕТОД РЕЗОЛЮЦИЙ
Метод резолюций в алгебре высказываний

7.

Пусть для некоторой переменной Х дизъюнкты
D1,D2 представимы в виде
.
Тогда дизъюнкт
называется резольвентой
дизъюнктов D1,D2 по переменной Х и
обозначается ResX(D1,D2).
По определению Res(X,
)=0.
Резолютивным выводом формулы Ф из
множества дизъюнктов S={ D1,...,Dm}
называется последовательность формул
Ф1,…,Фn, что Фn=Ф и каждая Фi либо
принадлежит S, либо является резольвентой
Res(Фk,Фj), 1≤j,k<i.

8.

Выполнимость логического следования
Ф1,Ф2,…,Фn |=Ф для формул Ф1,Ф2,…,Фn, Ф
равносильна Ф1,Ф2,…,Фn,¬Ф|=.
Лемма. Пусть формула Ф1 Ф2 … Фn ¬Ф для
формул Ф1,Ф2,…,Фn, Ф имеет КНФ D1 D2… Dk.
Тогда логическое следование Ф1,…,Фn|=Ф
выполняется тогда и только тогда, когда
множество дизъюнктов S={ D1,...,Dk}
противоречиво, т.е. существует резолютивный
вывод нуля из множества дизъюнктов S.

9.

АЛГОРИТМ ПРОВЕРКИ ЛОГИЧЕСКОГО
СЛЕДОВАНИЯ ФОРМУЛ Ф1,…,ФN|=Ф:
Составить формулу Ψ=Ф1⋀…⋀Фn⋀¬Ф
Найти ее КНФ Ψ=D1⋀…⋀Dm .
Найти резолютивный вывод значения 0 из
множества S={D1,…,Dm}. Если такой вывод
существует, то выполняется Ф1,…,Фn|=Ф.

10.

ПРИМЕР. МЕТОДОМ РЕЗОЛЮЦИЙ ПРОВЕРИМ
ЛОГИЧЕСКОЕ СЛЕДОВАНИЕ:
(¬X⟹Z),(Y⟹W),((W⋀Z) ⟹V), ¬V |= X ⋁¬Y,
Ψ=(¬X⟹Z) ⋀( Y⟹W) ⋀((W⋀Z) ⟹V) ⋀¬V⋀¬(X ⋁¬Y).
КНФ этой формулы:
(X ⋁ Z) ⋀(¬Y ⋁ W) ⋀ (¬W ⋁¬Z ⋁ V) ⋀¬V⋀¬X⋀Y.
Рассмотрим множество дизъюнктов полученной КНФ
формулы Ψ: S={X⋁Z, ¬Y⋁W, ¬ W⋁¬Z⋁V, ¬V, ¬X,Y}.
Построим резолютивный вывод значения 0 из этого
множества S:
Ф1=Resx(X ⋁ Z, ¬X)=Z,
Ф2=Resy(¬Y ⋁ W,Y)=W,
Ф3=Resz(¬W ⋁¬Z⋁V,Z)= ¬W⋁V,
Ф4=Resw(Ф2,Ф3)=V,
Ф5=Res(Ф4,¬V)=0.
Таким образом, множество дизъюнктов формулы Ψ
противоречиво и, значит, выполняется исходное
логическое следование.

11.

МЕТОД РЕЗОЛЮЦИЙ ДЛЯ
ИСЧИСЛЕНИЯ ПРЕДИКАТОВ

12.

Основные понятия метода резолюций для ИВ
естественно переносятся на ИП.
Пусть Xs − множество всех предметных переменных,
встречающихся в формулах из S, Cs – множество
констант, встречающихся в формулах из S, Fs –
множество всех функциональных символов,
встречающихся в формулах из S. Обозначим символом
As объединение множеств Xs и Cs.
На множестве As определим множество всех термов Ts
множества S.
Рассмотрим отображение : As Ts, которое определяет
подстановку термов t= (x) вместо переменных в
формулах из множества S, при этом на константы
отображение действует тождественным образом, т.е
(c)=c. Такое отображение принято называть
подстановкой и записывать в виде матрицы
В эту матрицу заносятся только те пары
(xi,ti)
(i=1,2,…,n), для которых ti= (xi)≠xi. Таким образом, для
всех x, которых нет в матричной записи подстановки,
предполагается, что (x)=x.

13.

Пример. Пусть формулы множества S содержат
константу c, переменные х,y, бинарный
функциональный символ f, тогда
подстановками являются следующие
отображения множества {x,y} в множество
термов TS:
Пример. Пусть формулы множества S содержат
константу c, переменные х,y, бинарный
функциональный символ f, терм t=f(x,y),
дизъюнкт D=P(x) T(x,y). Тогда результатом
действия на t,D подстановки
будут

14.

Пример. Композицией подстановок
является подстановка αβ=
Пусть Φ1,Φ2,…,Φk – множество атомарных формул,
которые встречаются в дизъюнктах множества S.
Если для подстановки γ выполняется
γ(Φ1)=γ(Φ2)=…=γ(Φk), то такая подстановка
называется унификатором множества формул
{Φ1,Φ2,…,Φk}, а само множество формул
{Φ1,Φ2,…,Φk} называется унифицируемым.
Пример. Рассмотрим множество формул
{P(x),P(f(c)),P(f(z))}, где P − унарный предикатный
символ, f – унарный функциональный символ, c –
константа. Подстановка
является
унификатором этого множества формул, поскольку
(P(x))= (P(f(c)))= (P(f(z)))=P(f(c)). Следовательно,
множество формул {P(x),P(f(c)),P(f(z))}
унифицируемо.

15.

БИНАРНАЯ РЕЗОЛЬВЕНТА
Пусть дизъюнкты D1,D2 из множества формул S не имеют общих
переменных и пусть L1 – некоторая литера в дизъюнкте D1, L2 –
некоторая литера в дизъюнкте D2. Если множество формул
{L1,¬L2} имеет унификатор , то дизъюнкт, который получается из
дизъюнкта (D1) (D2) вычеркиванием (или «отрезанием») литер
(L1), (L2), называется бинарной резольвентой дизъюнктов D1,D2
и обозначается Res(D1,D2).
В случае если (D1)= (L1), (D2)= (L2), полагают, что Res(D1,D2)=0.
Пример. Пусть D1=¬P(x) Q(y), D2=P(c) R(z) V(t), найдем
бинарную резольвенту D1,D2. Выберем литеры L1=¬P(x),L2=P(c),
тогда ¬L2=¬P(c). Множество формул {L1,¬L2} имеет унификатор =
Следовательно, бинарная резольвента дизъюнктов D1,D2
получается из формулы
(¬P(x) Q(y)) (P(c) R(z) V(t))=¬P(c) Q(y) P(c) R(z) V(t)
удалением литер ¬P(c) и P(c), т.е. Res(D1,D2)= Q(y) R(z) V(t).
Если же дизъюнкты D1,D2 из множества формул S имеют общие
переменные, то заменив их в дизъюнкте D2 на переменные,
которых нет в дизъюнктах D1,D2, получим дизъюнкт D, не
имеющий общих переменных с дизъюнктом D1.

16.

Пусть дизъюнкт D имеет вид 1 2 … l ,
где 1, 2,…, l – атомарные формулы,
−унификатор множества формул { 1, 2,…, l}.
Дизъюнкт ( 1) ( ) называется склейкой
дизъюнкта D. Аналогично, если дизъюнкт D
имеет вид ¬ 1 ¬ 2 … ¬ l , где 1, 2,…, l –
атомарные формулы, − унификатор
множества формул { 1, 2,…, l}, то дизъюнкт
¬ ( 1) ( ) называется склейкой дизъюнкта D.
Пример. Пусть дизъюнкт D имеет вид:
D=P(f(c)) P(x) P(f(y)) V(z). Тогда
унификатор множества атомарных формул
{P(f(c)),P(x),P(f(y))}. Дизъюнкт P(f(c)) V(z)
является склейкой дизъюнкта D.

17.

РАССМОТРИМ АЛГОРИТМ МЕТОДА РЕЗОЛЮЦИЙ ДЛЯ
ДОКАЗАТЕЛЬСТВА ЛОГИЧЕСКОГО СЛЕДОВАНИЯ Ф1,Ф2,…,ФN |=Ф,
ГДЕ Ф1, 2,…, N, − НЕКОТОРЫЕ ФОРМУЛЫ ИП.
1.
2.
3.
4.
5.
6.
Составить формулу Ф1 Ф2 … Фm ¬Ф.
Привести формулы Ф1,Ф2,…,Фm,¬Ф к сколемовским
стандартным формам.
Составить множество S дизъюнктов ССФ, найденных в п.2.
Продолжить (пополнить) последовательность дизъюнктов S
новой бинарной резольвентой Res(D1,D2), где D1,D2 – некоторые
дизъюнкты из множества S или склейки этих дизъюнктов.
Если получается нулевая резольвента, то множество формул
Ф1,Ф2,…,Фm,¬Ф противоречиво, а логическое следование
Ф1,Ф2,…,Фn |=Ф выполняется. Если нулевая резольвента пока
не получена, то перейти к шагу 4.
Если среди текущего множества дизъюнктов нет
резольвируемых, а нулевая резольвента не получилась, то
логическое следование Ф1,Ф2,…,Фn|=Ф не выполняется. Если же
процесс нахождения резольвент не останавливается, т.е.
множество дизъюнктов пополняется новыми резольвентами,
среди которых нет нулевых, то нельзя сделать вывод о
выполнимости или невыполнимости логического следования
Ф1,Ф2,…,Фn |=Ф.

18.

Пример. Докажем невыполнимость множества
формул W={Ф1, …,Ф6}, где
Ф1 =Р1(a,f(b),f(c)),
Ф2=Р2(а),
Ф3=Р1(х,х,f(x)),
Ф4=¬ Р1(х,у,z) ⋁P3(x,z),
Ф5=¬Р2(х) ⋁¬ Р1(у,z,u) ⋁¬P3(x,u) ⋁ P3(x,y) ⋁ P3(x,z),
Ф6=¬P3(а,с).

19.

Построим резолютивный вывод значения 0 из
этого множества W:
Ф7=Res(Ф2,Ф5)=Res(Ф2,
Ф5)=
= ¬ Р1(z,z,u) ⋁¬P3(a,u) ⋁ P3(a,z),
Ф8=Res(Ф3,Ф7)=Res(Ф3 ,
Ф7)= ¬P3(a,f(x)) ⋁ P3(a,x),
Ф9= Res(Ф6,Ф8)=Res(Ф6 ,
Ф8)= ¬P3(a,f(с)),
Ф10= Res(Ф4,Ф9)=Res(Ф9,
Ф11= Res(Ф1,Ф10)= Res( (
y
f (b)
Ф4)= ¬ Р1(а,y,f(c)),
) Ф10 ,Ф1)= 0.
Таким образом, построен резолютивный вывод
значения 0 из множества W. Значит, множество
дизъюнктов W={Ф1, …,Ф6} невыполнимо,
следствие выполняется.

20.

ИСТОЧНИКИ ИНФОРМАЦИИ:
Ершов Ю.Л., Палютин Е.А. Математическая
логика. – М.: Наука, 1987. 336 с.
Лихтарников Л.М., Сукачева Т.Г.
Математичекая логика. Курс лекций: Учебное
пособие. – СПб.: «Лань», 2008. – 288 с.
Молчанов В.А. Математическая логика:
учебное пособие. – Саратов: СГСЭУ, 2011.