1.9.5. Доказательство теорем методом резолюции в ип

1.9.5.1. Вывод новых импликаций из имеющихся

Высказывания, исходно считающиеся истинными, называются аксиомамиилигипотезами. Следующие из них высказывания называютсятеоремами.

Как правило, при доказательстве теорем производится вывод импликаций из других импликаций. Поэтому рассмотрим следующее. Пусть имеются две импликации:

H'₁(x_)^H'₂(x_)^...^H'_k(x_)C'₁(x_)C'₂(x_)...C'_l(x_)

H"₁(x_)^H"₂(x_)^...^H"_m(x_)C"₁(x_)C"₂(x_)...C"_n(x_),

где x_- константа из множества допустимыхx. Если какая-то формула из правой части одной импликации идентична формуле из левой части другой импликации:

C'_i(x_) = H"_j(x_), (*)

то справедливым будет утверждение:

(**)

Действительно:

H'₁(x_)^H'₂(x_)^...^H'_k(x_)C'₁(x_)C'₂(x_)...C'_l(x_) = ~(H'₁(x_)^H'₂(x_)^...^H'_k(x_))C'₁(x_)C'₂(x_)...C'_l(x_) = ~H'₁(x_)~H'₂(x_)...~H'_k(x_)C'₁(x_)C'₂(x_)...C'_l(x_)

(~H'₁(x_)~H'₂(x_)...~H'_k(x_)C'₁(x_)C'₂(x_)...C'_l(x_))(~H"₁(x_)~H"₂(x_)...~H"_m(x_)C"₁(x_)C"₂(x_)...C"_n(x_)) (***)

Таким образом, мы получили КНФ, с которой можно работать согласно известному принципу резолюций, т.к. она содержит только константы. Принцип резолюций позволяет применить формула (*) и тот факт, что эти два предиката оказались в выражении (***) взаимоинверсны. Формула (***) преобразуется в один дизъюнкт. В этом дизъюнкте все инверсные предикаты сворачиваются в инверсию конъюнкции согласно правилу де Моргана, откуда следует импликация (**).

Данный пример сильно упрощен. На практике встречаются следующие уточнения:

1. Дизъюнкты не обязательно содержат константы. В этом случае рассматривают не только идентичные, а вообще сопоставимые формулы (т.е. с одинаковыми предикатными именами). Переменные конкретизируются вплоть до получения идентичных формул из сопоставимых.

2. В общем случае правило резолюций допускает сопоставление не одной литеры из левой части одной импликации и из правой части другой, а нескольких.

Существует ряд стратегий доказательств, использующих метод резолюций и отличающихся алгоритмически.

Разберем стратегии доказательства теорем, использующие метод резолюций, на примере:

Аксиомы:

P1: Если X есть часть V и если V есть часть Y, то X есть часть Y.

P2: Палец есть часть кисти руки

P3: Кисть руки есть часть руки

P4: Рука есть часть человека

Доказать теорему: Палец есть часть человека.

1.9.5.2. Стратегия "сначала вширь"

Будем считать, что заданные аксиомы имеют уровень 0. Путем получения из них резольвент получаются предложения 1-го уровня вплоть до полного перебора возможных применений принципа резолюций. Предложения 2-го уровня получаются из предложений 0-го и 1-го уровней и т.д.

Имя предложения	Предложение	Основание
P1	Часть(X,V)  Часть(V,Y)Часть(X,Y) ~Часть(X,V)~Часть(V,Y)Часть(X,Y)	Задано
P2	Часть(палец, кисть руки)	Задано
P3	Часть(кисть руки, рука)	Задано
P4	Часть(рука, человек)	Задано
P5	~Часть(палец, человек)	Отрицание доказываемого
1-й уровень
P6	~Часть(кисть руки, Y)  Часть(палец, Y)	r[P2, P1]
P7	~Часть(рука, Y)  Часть(кисть руки, Y)	r[P3, P1]
P8	~Часть(человек, Y)  Часть(рука, Y)	r[P4, P1]
P9	~Часть(палец, V)  ~Часть(V, человек)	r[P5, P1]
2-й уровень
P10	~Часть(кисть руки, человек)	r[P2, P9]
P11	Часть(палец, рука)	r[P3, P6]
P12	Часть(кисть руки, человек)	r[P4, P7]
P13	~Часть(кисть руки, человек)	r[P5, P6]
3-й уровень
P14	#	r[P10, P12]

1.9.5.3. Стратегия "предпочтение - единичным элементам"

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

Имя предложения	Предложение	Основание
P1	Часть(X,V)  Часть(V,Y)Часть(X,Y) ~Часть(X,V)  ~Часть(V,Y)Часть(X,Y)	Задано
P2	Часть(палец, кисть руки)	Задано
P3	Часть(кисть руки, рука)	Задано
P4	Часть(рука, человек)	Задано
P5	~Часть(палец, человек)	Отрицание доказываемого
P6	~Часть(кисть руки, Y)  Часть(палец, Y)	R[P2, P1]
P7	Часть(палец, рука)	R[P3, P6]
P8	~Часть(кисть руки, человек)	R[P5, P6]
P9	~Часть(X, палец)  Часть(X, кисть руки)	R[P2, P1]
P10	~Часть(рука, Y)  Часть(кисть руки, Y)	R[P3, P1]
P11	Часть(кисть руки, человек)	r[P4, P10]
P12	#	r[P8, P11]

1.9.5.4. Стратегия опорного множества

Экспериментатор называет некоторые предложения аксиомами, а все остальные относит к опорному множеству. Резольвента не ищется для двух аксиом. Все другие резолюции допустимы.

Имя предложения	Предложение	Основание
P1	Часть(X,V)  Часть(V,Y)Часть(X,Y) ~Часть(X,V)  ~Часть(V,Y)  Часть(X,Y)	Задано
P2	Часть(палец, кисть руки)	Задано
P3	Часть(кисть руки, рука)	Задано
P4	Часть(рука, человек)	Задано
P5	~Часть(палец, человек)	Отрицание доказываемого
P6	~Часть(палец, V)  ~Часть(V, человек)	R[P1, P5]
P7	~Часть(кисть руки, человек)	R[P2, P6]
P8	~Часть(палец, рука)	R[P4, P6]
P9	~Часть(кисть руки, V)  ~Часть(V, человек)	R[P1, P7]
P10	~Часть(рука, человек)	R[P3, P9]
P11	#	R[P4, P10]