Вопросы_по_физике_3_сем_экз_Тронева / 13-14 new

13) В математической логике и автоматическом доказательстве теорем, правило резолюций – это правило вывода, восходящее к методу доказательства теорем через поиск противоречий; используется в логике высказываний и логике предикатов первого порядка. Правило резолюций, применяемое последовательно для списка резольвент, позволяет ответить на вопрос, существует ли в исходном множестве логических выражений противоречие. Правило разработано Джоном Аланом Робинсоном в 1965.Пусть C₁ и C₂ - два предложения в исчислении высказываний, и пусть , а , где P - пропозициональная переменная, а C'₁ и C'₂ - любые предложения (в частности, может быть, пустые или состоящие только из одного литерала).

Правило вывода называется правилом резолюции.

Предложения C₁ и C₂ называются резольвируемыми (или родительскими), предложение - резольвентой, а формулы P и - контрарными литералами.

14) Близким к методу резолюций является метод Вонга, в котором тоже исполь­зуется сконструированная конъюнктивно-дизъюнктивная нормальная форма представления исходной клаузы, а аксиому порядка заменяет клауза Вонга.

X, L=>X;R,

здесь X пробегает некоторые буквы, входящие в клаузу, a L и R—s определенные комбинации дизъюнктов и конъюнктов.

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

Разберем метод Вонга на примере доказательства справедливости правила отделения:

А, А -> В => В или A, -AvВ => В .

Здесь имеется только один дизъюнкт, который можно подвергнуть разбиению. После его разбиения получим две новых клаузы:

А, -А=>В и А, В =>В .

Вторая клауза удовлетворяет и аксиоме порядка и клаузе Вонга. В качестве Xв ней выступаетB,aL=AиR=0. Первая же клауза тоже будет удовлетворять необходи­мым требованиям, но только после того, как терм -А из левой части клаузы с противоположным знаком перенести в правую часть. Тогда будем иметь:

А => А; В

где X=A,L= 1 иR= В .

При большом числе букв в исходной клаузе прибегают к специальной нумерации производных клауз чтобы не запутаться. Пусть требуется установить справедли­вость следующей клаузы:

X v Y, (X -> Y) v U, Z -> (Y -> W) => (W -> X) -> (Z -> X).

Приведем ее в соответствующую конъюнктивно-дизъюнктивную нормаль­ную форму:

X v Y, -X v Y v U, -Z v -Y v W => W & -X; -Z; X .

Далее произведем разбиение первого дизъюнкта, в результате получим две производные клаузы:

1. X, -X v Y v U, -Z v –Y v W => W & -X; -Z; X

2. Y, -X v Y v U, -Z v –Y v W => W & -X; -Z; X

Клауза (1) отбрасывается, так как она удовлетворяет клаузе Вонга. Разбивая сле­дующий дизъюнкт клаузы (2), получаем еще три новых клаузы:

2.1. Y, -X, -Z v -Y v W => W & -X; -Z; X

2.2. Y, Y, -Z v -Y v W => W & -X; -Z; X

2.3. Y, U, -Z v -Y v W => W & -X; -Z; X

Клаузы (2. 1) и (2. 2) сводятся к одной клаузе —

1. Y, -Z v -Y v W => W & -X; -Z; X

Произведем ее разбиение:

2.1.1. Y, -Z=>W & -X; -Z; X

2.1.2. Y, Y => W & -X; -Z; X

2.1.3. Y, W => W & -X; -Z; X

Первые две клаузы удовлетворяют клаузе Вонга. У клаузы (2.1.3) нужно разбивать конъюнкт:

2.1.3.1. Y, W => W; -Z; X

2.1.3.2. Y, W => -X; -Z; X

Теперь обе клаузы имеют вид клаузы Вонга.

Но у нас осталась еще ветвь (2.3). Она отличается от рассмотренной ветви (наличием непарного терма U, который, однако, не может повлиять на конечный результат, т.е. разбиение клаузы (2.3) практически полностью совпадает с разбиением клаузы (2.1). Следовательно, исходная клауза была записана верно.