Intel_Nils (526801), страница 39
Текст из файла (страница 39)
Если подстановка 0 применяется к каждому элементу множества (Е») литералов, то множество соответствуюших ей частных случаев обозначается через (Е»)в. Множество (Е») литералов называется унифицируемым, если существует такая подстановка 8, что Е»в = Еоо = Езв = .. В этом случае подстановку О называют унификатором для (Е»), поскольку ее применение сжимает множество до одного элемента. Например, подстановка О = ((а, х), (Ь„у)) унифицирует множество (Р(х, 1(у), Ь), Р(х,((Ь),Ь)) и дает (Р(а,((Ь), Ь)). Унификатор О = ((а, х), (Ь,у)) для множества (Р(х,((у), Ь), Р(х,((Ь),Ь)) в некотором смысле не является простейшим.
За- 6.12. Унификация метим, что для унификации нет необходимости подставлять а вместо х. Наиболее общим (или простейшим) унификатороас (ноу) для ((н) будет такой унификатор Х, что если 8 — какойпибудь унификатор для (Ьс), дающий ((и)а, то найдется подстановка б, для которой (с„)аа = (с,а)а. «Общий» частный случай, соответствующий наиболее общему унификатору, единствен с точностью до алфавитных вариантсв. Существует алгоритм, называемый алгоритмом унификации, который приводит к наиболее общему унификатору для унифицируемого множества (с'.;) литералов и сообщает о неудаче, если это множество неунифицируемо. Схему работы алгоритма можно описать следующим образом. 'Алгоритм начинает работу с пустой подстановки ') и шаг за шагом строит наиболее общий унификатор, если таковой существует.
Предположим, что на й-м шаге получена подстановка Ха. Если все литералы множества (с.с) в результате применения к каждому нз них подстановки становятся идентичными, то Х = Ха и есть наиболее общий унификатор. В противном случае каждый из литералов в (с.с) рассматривается как цепочка символов и выделяется позиция первого символа, в которой не все из литералов имеют одинаковый символ. Затем конструируется множество рассогласования, содержащее п.п. выражения из каждого литерала, который начинается с этой позиции.
(П. п. выражение представляет собой либо терм, либо литерал.) Так, множеством рассогласования для (Р(а,((а, а(г)), Ь(х)), Р(а, ((а, и), я(ги))) 'т' будет (д (з), и). Далее алгоритм пытается так модифицировать подстановку )сь чтобы сделать равным два элемента из множества рассогласования. Это можно сделать только тогда, когда множество рассогласования содержит переменную, которую можно положить равной одному из его термов. (Если множество рассогласования вообще не содержит переменных, то множество ((.,) унифицировать нельзя. Например, на первом шаге работы алгоритма множество рассогласования может оказаться самим ((.с), и тогда ясно, что ни один из элементов не будет переменной.) Пусть ад — переменная в множестве рассогласования и 2а— терм (возможно, другая переменная) в множестве рассогласования, не содержащий за.
(Если такого 1а нет, то множество (с.с) неунифицируемо.) Теперь можно образовать модифицированную подстановку Ха+с = Ха((са, зд)) и выполнить следующий р б р ') То есть ие делается ааиаква подстааовоа. — Лрии иерее. Гл, б. Докавотельство теорем в исчислении нредикатов 1вс) Множество литерское «Общее» честные слтчен (Р (т), Р (а)) (Р (( (х), у, у (у) ), Р (((х), г, у (х) ) ) (Р (( (х, у (в, у)), д (а, у) ), Р() (х, г), г)) Р (а) Р (1 (х), х, д (х) ) Р (( (х, д (а, у) ), у (а, у)) Г!ринято рассматривать предложения как множества литералов. Тогда предложение, содержащее множество (СД литералов, можно также обозначить (г".ч).
Если подмножество литералов в некотором предложении (ьс) унифицируемо с помощью ноу ) то предложение Ща называют фактором предложения (т'.г). Факторами предложения Р(((х)) Ч Р(х) Ч (;)(а, ((и)) Ч (;)(х, ((Ь)) Ч Я(г, нс) являются, например, предложения Р(((г)) т/ Р(г) т/ Я(а, 1(и)) Ч Я(г, ((Ь)) и Р6 (а)) тес Р(а) ьг Я(а, ((Ь)). В первом факторе унифицированы только два последних вхождения литерала Я, а во втором все три. Заметим, что в этом предложении два вхождения литерала Р нельзя унифицировать.
Вообще предложение может иметь более одного фактора, но, во всяком случае, число факторов конечно. 6.13. Резольвенты Теперь опишем процесс, с помощью которого иногда можно вывести новое предложение из двух других (называемых исходными предложениями). Пусть исходные предложения задаются в виде ((и) и (Мг) и переменные, входящие в (Мс), не встречаются в ((и) и обратно' ). Пусть ((г) с:-[(и) и (лтч) ': — (й(г)— такие два подмножества в (Еч) и (й(е), что для объединения ((с) 0 ( лг,;) существует наиболее общий унификатор )ь. (Иными ') В любой паре предложений всегда можно тан переименовать перемен. ные, чтобы ато предположение выполнялось. Можно доказать (Робинсон, 1965а и Лакхэм, 1967), что описанный алгоритм находит наиболее общий унификатор для множества унифицируемых литералов и сообщает о неудаче, если литералы неунифицируемы, Мы не будем давать здесь доказательство этого утверждения.
В качестве примеров приведем «общие» частные случаи, соответствующие наиболее общему унификатору для ряда множеств литералов. влз. Реэольаенты словами, (тг)к содержит одиночный литерал, равный отрицанию одиночного литерала в ((<)ь) Тогда говорят, что два предложения (г.г) и (Мг) разрешаются, а новое предложение Н(ч) — ((г))л 0 ((Мг) — (вггйа является их резольвентой, Резольвента представляет собой выведенное предложение, н процесс образования резольвенты нз двух «родительских» предложений называется резольвенцией. Если два предложения разрешаются, то они могут иметь более одной резольвенты, поскольку способ выбора (Ц и (вЦ может оказаться не единственным. Но, во всяком случае, онн имеют не более конечного числа резольвент.
Сейчас мы дадим несколько примеров резольвенции и попытаемся связать ее с более знакомыми нам правилами вывода. Рассмотрим два предложения Щ=Р(х, )(а)) Ч Р(х,) (у)) Ч (;)(у) и (Мг)= Р(х,1(а)) ~/ ге(х). Выбирая подмножества ()г)=(Р(х,) (а))) и (вгг)=( Р(з,) (а))), мы получаем резольвенту Р (х. 1(у)) Ч -Я ( ) Ч Я(у) а если взять (Ц=(Р(х, 7(а)), Р(х, ) (у))) и (тг)=( Р(г, ((а))), то резольвентой будет (с (а) тг ге (2). Всего для этих двух предложений есть четыре резольвенты: три из них получаются разрешением на Р и одна разрешением на Я. Резольвеиция является общим правилом вывода, объединяющим подстановку, глобы ропепз') и различные типы силлогизмов. Рассмотрим резольвенту Я(а) двух предложений Р(а) Ч Я(а) и Р(а).
Если первое предложение записать в виде Р(а) Ф Я(а), то ясно, что в этом случае резольвенция совпадает с гпобцз ропепз. ') Мойна ролена — латинское название первой формы гипотетического силлогнэма, выражаемой формулой (А т/ (А -ь В)) - В (т. е. если иэ А следует В н А имеет место, то имеет место и В). — Прим.
Ред. 198 Гл. б. Докавателоство теорем в исчислении аредикатов Рассмотрим теперь резольвенту Р(х) чг(,)(х) двух предложений Р(х) ~/)с(х) и -)с(л) ~у Я(х). В более привычных обозначениях (а также на русском языке) эта цепочка рассуждений выглядит так: Обычная косяка На руссяоя языке (чгск) (Р (к) =)р К (к) ) ргк)(л (.) =р Е (.» Следовательно: (Ьгк) (Р (к) )ь Я (к) ) Все, что обладает свойством Р, имеет свойство гс Все, что обладает свойством )1, имеет свойство с) Все, что обладает свойством Р, имеет свойство Я Такой вывод является одним из силлогизмов. ') См, примечание г)а стр.
172. — Прим. перев. $.14. пРинцип РезОЛьвенции ') Резюмируем кратко основные идеи втой главы. Мы хотим иметь возможность находить доказательство того, что некоторая правильно построенная формула (е' в исчисленид пйедикат тов логически следует из некоторого множества 5 правильнсг построенных формул. Мы показали, что эта задач. эквивалентна задаче доказательства того, что множество ( ° йт) () 5 неудовлетворимо. Процессы выявления неудовлетворнмссти некоторого множества предложений называются процессалси опровержения.
Собираясь применять частный случай процесса опровержения, приложимый к п. п. формулам, имеющим форму предложений, мы привели простую последовательность операций, позволяющую представить любую и. п. формулу в виде предложений. Затем ввели понятие области, названной универсумом Эрбрана, для множества 5 предложений и объяснили, как использовать построенное на его основе семантическое дерево для представления всех интерпретаций предложений из 5. Если множество 5 неудовлетворимо, то, разумеется, нельзя найти интерпретацию, при которой все п. ц, формулы в 5 истинны.
На такую неудовлетворимость множества 5 указывает замкнутость его семантического дерева. Мы показали, как можно использовать общее правило вывода, называемое резольвенцией, для создания новых предложений. Дальше мы покажем, что при добавлении к 5 этих предложений у семантического дерева В,И, Принцип реэольеенции !йв для нового множества (по-прежнему неудовлетворимого) над неблагоприятными вершинами будет меньше вершин, и этот процесс можно продолжать до тех пор, пока не останется только корневая вершина, соответствующая неблагоприятной вершине для пустого предложения. Мы заключаем, что если продолжать осуществлять резольвенции на множестве неудовлетворимых предложений, то в р)х) ч О(х) -о)г<г)) пи) ип Рис. 6.3. Граф опровержеиия для невыполнимого множества (р(л)ЧЕ(х), -Е()(в)), -р()(е))нй(в), -))(м))- конце концов придем к пустому предложению.
Этот результат позволяет пользоваться в процессе опровержения одним только правилом резольвенции без явной ссылки на семантические деревья. Пусть Я(5) — объединение множества 5 с множеством всех резольвент всех пар его предложений. Пусть Яе(5) обозначает Я(Я(5)) и т. д. Если множество 5 неудовлетворимо, то мы гарантированы, что при некотором конечном и (называемом уровнем, или глубиной, опровержения) в Я" (5) будет пустое предложение. Так как множество Я'(5) при любом ( конечно, если конечно 5, то эта простая стратегия нахождения опровержения является конечным (хотя, быть может, долгим) процессом.
Образование множеств Я(5), Яэ(5), ... соответствует полному перебору при поиске опровержения. В гл. 8 мы обсудим различные стратегии поиска, более эффективные, чем эта простая стратегия. Опровержения, использующие резольвенции (иногда называемые доказательствами с помощью резольвенций), можно 200 Гл. 6. Докаэательстео теорем е исчислении иредикатоа проиллюстрировать графоподобными структурами, в которых в каждой вершине записано некоторое предложение. Предложения из 5 записаны в концевых вершинах этого графа.
Если два предложения, находящиеся в концевых вершинах, разрешаются, то их резольвента записывается в идущей непосредственно за ними вершине, которая соединяется с этими конце- -В(х) ч С(х) С(х) -С(с) н)1 Ряс. 6.4. Граф опровержения для невыполнимого множества (и (х), В(х) ~/ С(х), С(а) ~/1)(а), С(сМЕ(д), В(х) !/ о" (у)). выми'вершинами с помощью ребер. Корнем графа опровержения с помощью резольвенции (эти графы обычйо изображаются с корнем, расположенным внизу рисунка) служит пустое предложение (обозначаемое символом и!)).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
