Логике предикатов

Особенности метода резолюций при доказательстве теорем в

Идея Робинсона – автора метода резолюций, - состоит в том, чтобы в логике предикатов можно было, работать, непосредственно, с дизъюнктами, содержащими переменные, не прибегая к предварительной замене переменных константами из области определения . Эта идея обеспечивается использованием операций подстановки и унификации. Чтобы определить суть этих операций, введем несколько новых понятий и определений.

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

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

Пока нет никакой литеры в , контрарной какой-нибудь литере в . Однако, подставив в функцию вместо переменной , получим:

Теперь литера в контрарна литере в .

Следовательно, можно получить резольвенту из и :

Определение 1: подстановка – это конечное множество вида , где каждая - это переменная, каждый - терм, отличающийся от , а все - различны.

Определение 2: Пусть - подстановка, а - выражение. Тогда - это выражение, полученное из заменой одновременно всех вхождений переменной в выражении на терм . называется примером . Например, пусть и Тогда подстановка дает

Понятие «композиция подстановок». Пусть даны подстановки и Тогда композиция и есть подстановка , которая получается из множества вычеркиванием всех элементов , для которых и всех элементов таких, что . Рассмотрим пример определения композиции подстановок и . Тогда Однако по определению должна быть вычеркнута; и также должны быть вычеркнуты, так как и содержатся среди переменных подстановки . В итоге получаем

Понятие «унификатор для множества выражений». Подстановка называется унификатором для множества выражений тогда и только тогда, когда . Считается, что множество выражений унифицируемо, если для него существует унификатор.

Унификатор для множества выражений называется наиболее общим унификатором (НОУ) тогда и только тогда, когда для каждого унификатора для этого множества существует токая подстановка , что . Пусть, например, есть множество выражений . Тогда есть наиболее общий унификатор для , а есть унификатор.

Опишем по шагам алгоритм унификации, который находит НОУ, если множество унифицируемо, и сообщает о неудаче, если это не так [ 6 ]:

1) Установить и , где - пустая подстановка, не содержащая элементов. Перейти к шагу 2.

2) Если не является одноэлементным множеством, то перейти к шагу 3. В противном случае положить и окончить работу.

3) Каждая из литер в рассматривается как цепочка символов и выделяются первые подвыражения литер, не являющиеся одинаковыми у всех элементов , т.е. образуется так называемое множество рассогласований типа . Если в этом множестве - переменная, а - терм, отличный от , то перейти к шагу 4. В противном случае окончить работу с выводом: не унифицируемо.

4) Пусть и

5) Установить и перейти к шагу 2.

Рассмотрим работу алгоритма нахождения НОУ для множества Шаги следующие:

1) и

2) Так как не является одноэлементным множеством, то перейти к шагу 3.

3) Множество рассогласований т.е. замена

4)

5) Так как множество опять не одноэлементное, то множество рассогласований будет т.е. замена .

6)

7) Имеем , т.е. .

8)

Так как получено одноэлементное множество, то искомый наиболее общий унификатор .

Можно показать, что алгоритм унификации всегда завершается на шаге 2, если множество унифицируемо, и на шаге 3 - в противном случае.

Понятие «склейка дизъюнкта ». Если две или более литер (с одинаковым знаком) дизъюнкта имеют наиболее общий унификатор , то называется склейкой . Если - единичный дизъюнкт, то склейка называется единичной склейкой.

Пример: Пусть

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

Понятие «бинарная резольвента». Пусть и - два дизъюнкта (называемые дизъюнктами-посылками), которые не имеют никаких общих переменных. Пусть также и - две литеры соответственно в и . Если и имеют наиболее общий унификатор , то дизъюнкт называется бинарной резольвентой и , а литеры и называются отрезаемыми литерами.

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

Следовательно,

Таким образом, - бинарная резольвента и , а и - отрезаемые литеры.

Понятие «резольвента логики первого порядка». Резольвентой дизъюнктов-посылок и является одна из следующих резольвент:

1) бинарная резольвента и ;

2) бинарная резольвента и склейки

3) бинарная резольвента и склейки

4) бинарная резольвента склейки и склейки

Пример: Пусть ,

Тогда склейка дизъюнкта есть и резольвентой для и будет Вернуться

Дата добавления: 2014-01-04