Логике предикатов
Идея Робинсона – автора метода резолюций, - состоит в том, чтобы в логике предикатов можно было, работать, непосредственно, с дизъюнктами, содержащими переменные, не прибегая к предварительной замене переменных константами из области определения . Эта идея обеспечивается использованием операций подстановки и унификации. Чтобы определить суть этих операций, введем несколько новых понятий и определений.
Понятие «выражение». Под выражением понимается терм, множество термов, множество атомов, литера, дизъюнкт, множество дизъюнктов. Когда в выражении не встречаются никакие переменные, оно называется основным выражением: основной атом, основная литера, основной дизъюнкт, основной терм, что говорит об отсутствии в них переменных.
Понятие «подстановка». Предварительно на примере выясним, в чем состоит проблема поиска контрарных пар в логике предикатов. Рассмотрим следующие дизъюнкты:
Пока нет никакой литеры в , контрарной какой-нибудь литере в . Однако, подставив в функцию вместо переменной , получим:
Теперь литера в контрарна литере в .
Следовательно, можно получить резольвенту из и :
Определение 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) бинарная резольвента склейки и склейки
Пример: Пусть ,
Тогда склейка дизъюнкта есть и резольвентой для и будет Вернуться