Intel_Nils (526801), страница 40
Текст из файла (страница 40)
На рис. 6.3 приведен пример графа опровержения для множества неудовлетворимых предложений. Здесь для опровержения необходимы 3 резольвенции. Другой пример приведен на рис. 6.4. (Заметим, что на рис. 6.4 предложение С(х) используется на графе дважды. Иногда эти графы изображают в виде деревьев, повторяя поддеревья, появляющиеся более одного раза.) бдц Непрогиворенивоегь и нолнога рееольвеняии 20! влв. НЕПРОТИВОРЕЧИВОСТЬ И ПОЛНОТА РЕЗОЛЬВЕНЦИИ В этом разделе мы покажем, чтц принцип резольвенции не- противоречив и полон. Непротиворечивость означает, что если когда-нибудь мы придем к пустому предложению, то исходное множество обязано быть неудовлетворимым.
Полнота означает, что если исходное множество неудовлетворимо, то в конце концов мы придем к пустому предложению, Для того чтобы показать непротиворечивость принципа резольвенции, нужно доказать, что резольвента двух предложений логически следует из этих предложений, т. е. в прежних обозначениях, что ((ВД вЂ” ((ь))х() ((МД вЂ” (тД]„логически следует из (е.Д и (МД. Заметим, что каждая интерпретация, удовлетворяющая ((.Д и (МД, удовлетворяет ().Д„и (МД„.
Но поскольку никакая интерпретация не может удовлетворять одноврелеенно и ((ь)„и (тДЬ то каждая интерпретация, удовлетворяющая ((.Д н (МД, удовлетворяет также и нх резольвенте. Таким образом, резольвента логически следует из тех предложений, на которых она построена. Для того чтобы показать, что принцип резольвенции полон, достаточно показать, что он полон по отношению к вершинам вывода в семантических деревьях.
Обозначим через Тг замкнутое семантическое дерево для невыполнимого множества предложений 5, и пусть л — такая вершина вывода в Тг, что и, и пе — неблагоприятные вершины, расположенные непосредственно под п, но ни одно предложение нз 5 не терпит неудачу ни на и, ни выше и. Предположим, что предложение (АД из 5 терпит неудачу на пь а предложение (ВД' из 5 терпит неудачу на па. Тогда в данном случае полнота принципа резольвепции означает существование резольвенты для (АД и (ВД, скажем (СД, терпящей неудачу на вершине и или выше иее.
Нетрудно видеть, что такая резольвента существует. В самом деле, пусть е'. — элемент эрбрановской базы, значение истинности которого присваивается как раз под вершиной и. Пусть для определенности значение е. будет истинным для ль и ложным для пе. Хотя ни (АД, ни (ВД не терпят неудачу на вершине л, (АД терпит неудачу на пь а (ВД вЂ” на пг, Рассмотрим сначала предложение (АД.
Так как оно терпит неудачу на пь оно должно содержать по крайней мере одно унифицируемое подмножество, скажем (аД, для которого е". будет «общим» константным частным случаем. Пусть о — такой унифнкатор,что(а,)„= -1.. Далее, предложеиие (АД вЂ” (а;) терпит неудачу на вершине и (или выше нее), поскольку при переходе от и к и, мы лишь определили значение истинности для 1„ а (АД терпит неудачу на ль Аналогично, поскольку предложение [ВД терпит неудачу на ль оно должно содержать унифицируемое подмножество, Гл. 6. Докааателастео теорем е исчислении аредикагое скажем (Ьт], для которого Е будет «общим» константным частным случаем.
Пусть т — такой унификатор, что (Ьг], = т'.. Предложение (Вт) — (Ьт] также должно терпеть неудачу на вершине л (или выше нее). Теперь унификаторы о и т можно скомбинировать, поскольку переменные в (Аг) и (Ь«) можно считать различнйми. Обозначим этот комбинированный унификатор через оз. Таким образом, так как (аг)„= Т. и (Ьг) = Ь, то (Аг] и (Вг) имеют резольвенту ЦАг] — (аг)]к Ц ЦВз) — (Ьг)]к, где )ь — наиболее общий унификатор для (аг) () ( — Ь;). Так как Х вЂ” наиболее общий унификатор, то ЦАг] — (аг)] — частный случай предложения ЦАт) — (аг)]м а ЦВг) — (Ьг]]„— частный случай предложения ЦВг) — (ЬД]к Тогда, так как оба предложения ЦАз] — (ат]] и ЦВг] — (Ь)] терпят неудачу на вершине вывода п (или выше нее), то должны терпеть неудачу и предложения ЦАг) — (а4к и ЦВг] — (Ь;Ит,.
Очевидно, что их объединение— наша резольвента — также терпит неудачу. Для иллюстрации связи между семантическими деревьями и резольвентными построениями обратимся снова к множеству предложений 5, семантическое дерево которого изображено на рис. 6.2. Мы уже показали, что на вершине 1 терпит неудачу предложение Р(х) Л (г(х), на вершине 2 — предложение сс(1(у)), а их резольвента РЦ(у)) терпит неудачу на вершине 3 — вершине вывода. Далее, на семантическом дереве для множества 5,'= ( РЦ(у))) () 5 неблагоприятными вершинами будут вершины 3 и 4.
На вершине 4 терпит неудачу предложение РЦ(у)). Построение резольвенты для РЦ(у)) и РЦ(у)) приводит, разумеется, к пустому 'предложению (терпящему неудачу на корневой вершине). Итак, доказательство невыполнимости заканчивается всего лишь после двух резольвеиций. 6Л6. БИБЛИОГРАФИЧЕСКИЕ И ИСТОРИЧЕСКИЕ ЗАМЕЧАНИЯ Основания логики Наше весьма поверхностное изучение математической логики можно углубить, обратившись к некоторым стандартным учебникам. Блестящими учебниками являются книги Мендельсона (!964) и Роббина (!969)'), а для специалистов — классическая книга Черча (!956), В этих книгах излагается то, что можно назвать классической логикой.
Принцип резольвенций (или в действительности любое обсуждение автоматического доказательства теорем) еще не попал в учебники по логике. '! На русском языке можно порекомендовать монографию П. С. Новикоаа «Элементы математической логнкн», М., 1969. — Прим. ред. одо. Биоеиографические и исторические еаиечакие ЮЗ В основу настоящей главы мы положили исчисление предикатов первого порядка с резольвенциями, поскольку оно явно играет большую роль прн автоматическом решении задач. Существенное упущение здесь, однако, состоит в том, что мы не рассмотрели отношения равенства.
Все еще неясно, как «встроить» в автоматические доказатели теорем отношение равенства (и другие стандартные часто встречающиеся отношения). Обсуждение этих усложнений выходит за рамки настоящей книги. Одна нз схем, позволяющая включить отношение равенства в устройства автоматического доказательства теорем, обсуждается Робинсоном н Восом (1969). Далее, становится все яснее, что для создания сложных универсальных решающих устройств необходимо привлечь логики высших порядков. Обсуждение применения логики высших порядков к решению задач можно найти у Маккарти и Хэйеса (!969).
В книге Роббина (1969) есть раздел, посвященный логике второго порядка, а в статьях Дж. Робинсона (1969а, 19696) рассматриваются общие проблемы процедур доказательства для логик высших порядков. Этапы, выделенные нами при преобразовании правильно построенной формулы в совокупность предложений, основаны на процедуре Дэвиса и Путнама (1960). Такое представление 'в виде предложений называют также бескванторной коиъюнктивно нормальной формой.
Эрбрановские процедуры доказательства н резольвеиция Принцип резольвенцнй в автоматическом доказательстве теорем основан на процедуре доказательства Эрбрана (1930). Прямая реализация эрбрановской процедуры была бы в высшей степени неэффективной. Усовершенствования, внесенные Правицем (!960) и другими, привели в конечном итоге к принципу резольвенции. Дж.
Робинсона (1965а). Наш способ изложения методов доказательства, основанных на резольвенциях, опирается на работу Ковальского н Хэйеса (1969). (См. также Дж. Робинсон, !968.) Привлечение семантических деревьев делает очевидной связь между резольвенциями и эрбрановскими методами, их можно использовать также для доказательства применимости правил, более общих по сравнению с простой резольвенцней. Наше доказательство полноты принципа резольвенции является частным случаем доказательства полноты более общего правила вывода, приведенного у Ковальского н Хэйеса (!969). Ясно написанное, сжатое изложение принципа резольвенции с доказательством его полноты и непротиворечивости дано в статье Лакхэма (1967).
Доказательство непротиворечивости и полноты можно найти еще в первой работе Дж. Робинсона (1965а). В этих двух работах приведено также докйзательство 204 Гл. б. Доказательство теорем в исчислении арвдикагов «корректности» алгоритма унификации. Дж. Робинсон (1970) написал, кроме того, блестящее, исследование, посвященное «механическому доказательству теорем». Задачи 6.1.
Придать следуюшнм п.п, формулам вид предложений: а) (Ух) (Р(х) =1Э Р (х)), Ь) ( ((тгх) Р (х))) =(ь (их) ( Р (х)), с) -((1гх) (Р (х)ф((мр) (Р (р) =РР 0 (х, р))) Л-(тгу) я (х р)М Р (р))))) б) (ь! Вр)ИР(,р) =?э 0(р )) л(0(р, ) =) 3( ° у)))Ф =)ь (ВхЬ!р) (Р (х, у) =Ь Ю (х, у)). 6.2. При каких условиях универсум Эрбраиа для множества предложений 8 конечен? еб.в Напишите программу для приведення п.п. формулы к виду предло- жений.
6.4. Пусть Я вЂ” множество литералов и й — подстановка. Напишите про- грамму для вычисления Яр. 6.6. Исчисление высказываний можно рассматривать как частный случай исчисления предикатов, ногда единственными прединатными буквами яв- ляются пропозицнональиые символы рг (см. стр.
173). Как надо находить. з резольвенцню двух классов в исчислении высказываний? Возьмите отрицание каждой нз следуюших формул исчисления высказываний и используйте прин- цип резольвенции лли доказательства неудовлетворнмости множества предло- жений, получаемого из каждого таяого отрицания. а) 1Р ~/ Я) ~ (Я ~/ Р), Ь) (Р =)Ь Ц) ~ ((Р 'т' Р) =(Э О? 'т? <~)), с) ( Р =ф Р) =ф Р, д) (-0 =ф- Р) =Р ((-0 =)э Р) =?э а* е) ((Р =)Ь 17) =р Р) ~ Р, е6.6.
Определите точно (скажем, с помопгью блок-схемы) алгоритм унифи- кации, работаюший в соответствии с общим описанием в равд. 6.12. Исполь- зуйте этот алгоритм для поиска уиификатора множества (Р (х, х, у), Р (ш, и, ш), Р (а, и, и)). (Замечание: будьте внимательны при точном определении композиции под- становок.) Верно ли Ваш алгоритм обнаруживает тот факт, что множество. (Р(х), Р(((х))) не унифицируемо? Используя свой алгоритм, составьте про- грамму, выдаюшую наиболее общий унификагор множества 3, если оно уни- фицируемо, и п1! в противном случае. 6.7. Пусть С1 и Сэ — два предлохйэния. Покажите, как использовать про- граммы задач 6.4 и 6.6 дли написании программы вычисления множества всех реэольвент предложений С, и Сь 6.8.
Возьмите отрицание каждой из следующих теорем исчисления вреди- катов н используйте принцип резольвенцни для поиска противоречия; а) ( тх)(Р (х) ф Р (х)), Ь) ( ((т(х) Р (х))) и(Э (Чх) ( Р (х)), с) ((тх)(Р(х) Л 9 (х)) ~ ((гйх) Р (х)) Л ((Ь!у) с) (р)), б) ((Вх)(ту) Р (х, р)) =(? ((Уу) (Лх) Р (х, у)). Глава 7 ;ПРИМЕНЕНИЯ ИСЧИСЛЕНИЯ ПРЕДИКАТОВ К РЕШЕНИЮ'ЗАДАЧ 7.Е ИСЧИСЛЕНИЕ ПРЕДИКАТОВ ПРИ РЕШЕНИИ ЗАДАЧ В настоящей главе мы рассмотрим, как можно применить к решению задач доказательства теорем в исчислении предикатов. Иногда достаточно только знать, следует ли логически п. п.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
