Метод резолюций в логике предикатов

Метод резолюции состоит в следующем. Пусть имеется два предложения С1=A1∨…∨Am∨D и C2=B1∨…∨Bn∨D, содержащих один и тот же атом D. Резольвентой предложений C1 и С2 является предложение С=A1∨…∨Am∨B1∨…∨Bn. Если литералы D и D' не равны, но существует унификатор, делающий их равными, то наиболее общий унификатор для D и D' применяется к предложениям C1 и С2, а затем вычисляется их резольвента. Если резольвента C пуста, то это указывает на невыполнимость исходной формулы.

В случае нехорновских дизъюнктов метод резолюции необходимо дополнить правилом факторизации, применяемым для устранения повторяющихся литералов в одном предложении. Если литералы не равны, то также выполняется их унификация.

Рассмотрим простой пример. Пусть брадобреи бреют всех людей, которые не бреются сами и не бреют тех, кто бреется сам. Тогда брадобреи не существуют.

A1: ∀x Бб(x)⇒∀y(Б(y,y)⇒Б(x,y))

A2: ∀x Бб(x)⇒∀y(Б(y,y)⇒Б(x,y))

B: ∃x Бб(x)

После перевода в сколемовскую конъюнктивную нормальную форму получаем предложения:

C1: Бб(x)∨Б(y,y)∨Б(x,y)

C2: Бб(x)∨Б(y,y)∨Б(x,y)

C3: Бб(a)

Применяя метод резолюции и правило факторизации, получаем предложения:

C4: Бб(x)∨Б(x,x) факторизация C1

C5: Бб(x)∨Б(x,x) факторизация C2

C6: Б(a,a) резольвента C3 и C4

C7: Б(a,a) резольвента C3 и C5

С8: ⊥ резольвента C6 и C7

Исчисление предикатов. Язык и правила вывода исчисления предикатов.

Чтобы построить новое исчисление, нам требуется указать 3 компонента: язык, аксиомы и правила вывода.

Язык

Добавим к языку исчисления высказываний новые конструкции с предикатами и получим язык исчисления предикатов. Вот расширенная грамматика:

§ <выражение>::= <импликация>

§ <импликация>::= <дизъюнкция> | <дизъюнкция> <импликация>

§ <дизъюнкция>::= <конъюнкция> | <дизъюнкция> <конъюнкция>

§ <конъюнкция>::= <терм> | <конъюнкция> & <терм>

§ <терм>::= <предикат> | <предикат> (<аргументы>) | <переменная><терм> | <переменная><терм>

§ <аргументы>::= <переменная>

§ <аргументы>::= <переменная>,<аргументы>

Добавились 3 новых сущности:

(a) индивидные переменные --- мы будем записывать их маленькими латинскими буквами из начала алфавита

(b) предикаты (они обобщили пропозициональные переменные)

(c) кванторы: всеобщности () и существования ().