Резолюция с абстракцией

Методы доказательства теорем, основанные на абстракции, были предло­жены в [Plaisted, 1981], где использовалась идея аналогии, заключающаяся в том, что данная проблема А преобразуется в более простую проблему В, Далее, если А имеет решения, то и В имеет решения, причем структура одного из решений для В аналогична структуре решений для А. Поэтому решения для

97 4-6943

В можно использовать как руководство в поиске решений для А, Конечно, может случиться, что В имеет решения, даже если А их не имеет.

Как и раньше, полагаем, что дизъюнкт С, поглощает дизъюнкт С₂, если имеется подстановка в, такая, что CYEJeCa (6\9 называется примером дизъ­юнкта Си если 9 — константная подстановка, то Cfi называется фундаменталь­ным примером дизъюнкта С\).

Абстракцией называется соотнесение множества дизъюнктов /(С) с любым дизъюнктом С, таким, что / обладает следующими свойствами: 1) если дизъ­юнкт Сз является резольвентой дизъюнктов Су и С₂ и /?₃е/(С₃), то сущест­вуют Di^f(Ci) и £>₂е/(С₂), такие, что некоторая резольвента дизъюнктов А и D₂ поглощает D₃; 2) /(П) = {П}; 3) если C_t поглощает С₂, то для любой абстракции D₂ дизъюнкта С₂ имеется абстракция Д дизъюнкта Си такая, что D\ поглощает D₂. Если / является отображением, обладающим этими свойства­ми, то оно называется отображением абстракций. Если £>е/(С), то D называ­ется абстракцией дизъюнкта С. Абстракции обычно удовлетворяют свойству, что любой D в /(С) является тавтологией, если дизъюнкт С — тавтология.

Для конструирования абстракций в [Plai.sted, 1981] доказана следующая теорема. Пусть F — множество отображений литер на литеры. Предположим, что для всех OeF и для всех литер L имеет место Ф(~ ]Ц— |Ф(£).Если

С —дизъюнкт, то Ф(С) = {Ф(£): Z,eC}. Предположим также, что если дизъ­юнкт D является примером дизъюнкта С, то для всех Ф^еР существует Ф\^Р, такое, что Фг(") является примером <Ь\{С). Определим / через /(С)= = {Ф(С): Фе/⁷}. Тогда / является отображением абстракции.

Имеются синтаксические и семантические абстракции. Примерами синтак­сических абстракций служат фундаментальная абстракция, пропозициональная абстракция, абстракции, связанные с переименованием предикатных и функцио­нальных букв, с изменением знака литер, с перестановкой и вычеркиванием некоторых аргументов у предикатов или функций. Если С — дизъюнкт, то f(C) = {C':C является фундаментальным примером для С) есть фундамен­тальная абстракция.

Пропозициональная абстракция определяется следующим образом. Пусть С —дизъюнкт вида L\\JL%\'.:.\/Lk. Тогда f(C) есть {С}, где С — дизъюнкт вила WX«'V... VW и L_t'(l<i<k) есть Р, если L_t есть P(t_u t₂,...,t_n), и IP, если L_{ есть ~\P(tt, t₂,...,t_n), т. е, получаем дизъюнкты для исчисления высказываний. Специальным случаем этой абстракции является абстракция, связанная с вычеркиванием переменных (необязательно всех).

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

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

Семантическая абстракция связана с интерпретацией множества дизъюнк­тов, в котором означиваются все переменные функций и предикатов.

Покажем на примерах, как используются абстракции при доказательстве. Рассмотрим доказательство R(a) на дереве вывода (рис. 2.6,а) и с помощью пропозициональной абстракции (рнс. 2.6,6). Однако, применяя эту же пропо­зициональную абстракцию к доказательству другого дизъюнкта, получаем дока­зательство, неадекватное исходному, как это будет видно из следующего примера.

Для дерева вывода (рис. 2.7,а) применяем пропозициональную абстракцию. Получаем дерево вывода на рис. 2.7,6. Здесь имеет место потеря литеры ~~\Р(6). Во избежание таких потерь используем понятие мультидизъюнкта, в котором одна и та же литера может встречаться более одного раза, т. е., например, для дизъюнкта ~lP(a)V~l£4*)VQ(£) мультндизъюнкт, полученный пропозициональной абстракцией, будет иметь вид 1 PV ^PVQ- Тогда, продол­жая пример и используя понятие мультнднзъкжкта, нетрудно получить вывод QVR. 98

1PVQVR

Рис. 2.6

Pib)\jR(d)

6)

Рис. 2.7

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

В [Plaisted, 1981] было разработано несколько вариантов полных алгорит­мов доказательства теорем, основанных на абстракциях.

Поиск по сайту: