Intel_Nils (526801), страница 42
Текст из файла (страница 42)
Хотя этот метод и прост, но у него есть несколько тонких моментов, которые мы разъясним на примерах. П р и м е р 1. Рассмотрим правильно построенные формулы 1) (Ухну) ((Р (х, у) Л Р (у, г)) )т О (х, г)), 2) (Уу=)х) (Р (х, у)). Их можно интерпретировать так: 1) Для всех х и у, если х является родителем у и у является родителем г, то х является прародителем г 2) Каждый индивид имеет своего родителя. Будем считать эти формулы гипотезами и зададим такой вопрос: «Существуют ли такие индивиды х и у, что 6(х,у)?» (Иными словами, суи1ествуют ли такие х и у, что х является прародителем у?) Сформулируем этот вопрос в виде предположения, требующего доказательства: (Зх=)у) 6 (х, у). Это предположение легко доказать методом опровержения с помощью резольвенций, показав невыполнимость множества предложений, получаемых из аксиом и предположения. Дерево опровержения изображено на рис.
7.3. Литералы, подвергающиеся унификации при каждой из резольвенций, подчеркнуты. Подмножество литералов в предложении, подвергающееся унификации в процессе резольвенции, назовем множеством унификации. 210 Гл. 7. Применения исчисления предикатов к решению подач р(х„у) ч Р(у,г) ч щг) (. () -О(и.о) (оюрици и е преупаппэеепип! »р(и,у) и --р(о,о св) св) Р(и, Г(оу Рис.
7.З. Дерево опровержения для примера 1. Заметим, что предложение Р((((в),в) содержит сколемову функцию (, введенную при исключении квантора существования в аксиоме 2: (Чих)(Р(х, у)). Эта функция определяется' так, чтобы (1(у) (Р(((у),у). (Функцию ( можно интерпретировать как функцию, задающую имя родителя каждого индивида.) Модифицированное дерево доказательства приведено на рис. 7.4, Отрицание предположения преобразовано в тавтологию, а резольвенции осуществляются те же самые,.что и на рис. 7.3.
Каждая резоловенция в модифицированном дереве опирается на множества унификации, которые в точности соответствуют множествам унификации графа опровержения. Множества унификации на рис. 7.4 подчеркнуты. В корневой вершине дерева доказательства, изображенного на рис. 7.4, находится 6(((((о)), о). Это предложение соответствует п. п, формуле (эео)(((()(((о)), о)), представляющей собой ответное утверждение. Ответное утверждение дает полный ответ на вопрос: «Существуют ли такие х и у, что х является прародителем уу» Ответ в данном случае содержит определительную функцию (: любое о и родитель родителя этого и служат примерами индивидов, удовлетворяющих условиям вопроса.
Снова ответное утверждение имеет форму, близкую к форме вопроса. 7.8, Процесс. извлечения ответа иСуии,и) Ч С(и,и) (р,с) ч С(и.д) р(и,р) ч -р(и,са ч С(и,и( ~Ри Г ч С(и.и) С(Г(Г(в)) иР р в с. 7дк Моднфвцврованное дерево доказательства для примера 1. Пример 2. Покажем, как преобразовать в тавтологии более сложные предложения, возникающие при отрицании предположения. Рассмотрим следующее множество предложений: А(х) Ч Р(х) ~( 6(((х)), Р(х) ~/ В(х), Р (х) Ч С (х), б (х) Ч В (х), б (х) 1( Ю (х), А(д(х)) Ч Р(Ь(х)). Мы хотим доказать, исходя из этих аксиом, предположение (Лхасу) ((В (х) Л С (х)) Ч (Ю (у) Д В ((())). Отрицание его приводит к двум предложениям, каждое нз которых содержит по два литерала: В (х) 1( С(х), В(х) Ч Х)(х).
Граф опровержения для нашего дополненного множества предложений приведен на рис. 7.5. Теперь для преобразования графа мы должны превратить предложения, вытекающие из отрицания высказанного предположения (на рис. 7.5 они заключены в рамку), в тавтологии, дописав к ним их отрицания. В данном случае отрицания 212 Гл. 7. 7(рииеиеиия искислекия иредикатое к реи~екию еадач содержат знак Л. Предложение В(х) Ч С(х), например, преобразуется в формулу В(х) ~/ С(х) Ч (В(х) Л С(х) ).
Эта формула не будет предложением из-за имеющейся в ней конъюнкции (В(х) Л С(х) ). Однако мы будем обращаться с этой конъюнкцией, как с единым литералом, и действовать формально так, как будто наша формула является предложением (нн р(к( -Г(я( ч с(к( -а( (ч о(к( -т"(я( ч С(к( С(к( ч В( '( а(ян ч г(а(я() пц Рве. 7.5. Граф опровержении дяп примера 2. один нз элементов рассматриваемой конъюнкции не может оказаться нн в одном множестве унификации).
Аналогично преобразуем предложение -В(х) Ч В(х) в тавтологию В(х) Ч -В(х) ~/ (0(х) Л В(х)). Выполняя резольвенции, диктуемые соответствующими множествами унификации, мы строим граф, изображенный на рнс. 7.6. В корневой вершине расположена п.п. формула ((Ух)[В(И(х)) Л С(й'(х))! Ч [В(((Ы(х))) Л В(((К(х)))] ~/ Ч [В (й (х)) Л С (й (х))[). Мы видим, что здесь ответное утверждение имеет форму, нескольно отличную от формы, в которой было сделано предпо- 7.8.
Процесс извлеыеиии ответа ложение. Нетрудно видеть, что подчеркнутая часть ответного утверждения аналогична по форме всему предположению, но только здесь вместо переменной х, относящейся к квантору существования, стоит д(х), а вместо переменной у, относящейся к другому квантору существования, стоит )(у(х) ). Но в рассматриваемом примере в ответном утверждении имеется дополни- Вре ч С)х) ч ГИ)х) л В(х)) -С) )ч В( ). т")х) Ч С(Я Ч (В)х) Л С(хЦ -ртх) ч С)х) е Р)х)) ч Рдтх) Л С)ху -С)х)Ч)С( ) Л В) П р)агх))г )В)х)))) (В(й)Х)) ЛС(ЫХ)))Ч (В%В) )И Л ВЯВ)х))В Ч (В)В(х)) Л СЯ(х))) Рис. 7.й. Модифииироваииый граф доказательства дли примера з. тельный дизъюнкт (В(Ь(х)) Л С(Ь(х))).
Этот дизъюнкт похож на один из дизъюнктов, содержащихся в предположении, причем вместо переменной х, относящейся к квантору существования„здесь стоит й(х). Вообще, если предположение делается в днзъюнктивно нормальной форме, то в процессе извлечения ответа создается утверждение, представляющее собой дизъюнкцию выражений,. каждое из которых имеет форму либо всего предположения, либо одного или нескольких дизъюнктов этого предположения. Поэтому мы и говорим, что такое утверждение можно. 2!4 Гл.
Х Применения исчисления нрединатав и решению задач использовать в качестве «ответа» на вопрос, представляемый исходным предположением. Ситуацию, возникающую в общем случае, можно описать точно. Допустим, что нам нужно доказать предположение, имеющее вид Ях!) ... Яхн) [1Г! (х„..., хн) ~/ ... '!/ яр (х!...., хн)), где каждый член йг! представляет собой конъюнкцию литералов, Это значит, что каждый член )чг! можно записать в виде У'! = Е!! Л Е!з Л ° Л Ь!в! где переменные явным образом не указаны. Отрицание предпо- ложения приводит к предложениям После того как построен граф опровержения, каждое вхождение 'любого из этих предложений преобразуют в тавтологию, добавляя отрицание предложения.
Иными словами, добавляют формулы вида 1.!! Л ~ез Л ... Л ~.!в — — Вгс(х!, хм ..., Хн). Таким образом, в корневой вершине преобразованного графа опровержения будет'получено ответное утверждение, состоящее нз дизъюнкций членов !Р !, в которых вместо переменных х!, ..., х„стоят различного рода частные случаи.
Ясно, что каждый член )в! может вовсе не содержаться в ответном утверждении, а может содержаться в нем один или даже несколько раз. Таким образом, совсем не обязательно, чтобы ответное утверждение имело вид в точности как у предположения. 74. ПРЕДПОЛОЖЕНИЯ, СОДЕРЖАЩИЕ ПЕРЕМЕННЫЕ, ОТНОСЯЩИЕСЯ К КВАНТОРУ ВСЕОБЩНОСТИ В случае когда предположение, которое требуется доказать, содержит переменные, относящиеся к квантору всеобщности, возникают дополнительные трудности. При отрицании такие переменные переходят в переменные, относящиеся к квантору существования, а это приводит к необходимости введения сколемовых функций. Что должно служить интерпретацией этих сколемовых функций, если они в конце концов появляются в качестве терман в ответном утверждении? 74.
Предположения с нвантором всеобщности 2!5 Проиллюстрируем это на примере. Зададим аксиомы в виде предложений; 1) С(х, Р(х)): каждый х является ребенком для Р(х). (Иными словами, Р— функция, ставящая в соответствие ребенку индивида самого индивида.) 2) С(х, у) ~( Р(у, х): для всех х и у, если х — ребенок для у, то у — родитель для х. Теперь мы задаем вопрос: «Для любого х кто является его родителем?» Предположение, соответствующее этому вопросу, имеет вид ~ухну) Р(у, х). Преобразуя отрицание этого предположения в форму предложений,мы получаем сначала Дну) Р(у, х), а затем Р(у, а), где а — сколемова функция, не содержащая аргументов (т.
е. константа), введенная для исключения квантора существова- С(л.у) Ч робя) л Р(у,а) -С(а т) и р(у,а) С(яр(лу) р(р(ада) Р н с. 7.7. Модифицированное дерево доказательства для получения ответ- ного утверждения. ния, появляющегося при отрицании предположения. (Отрицание предположения означает, что некоторый индивид, а не имеет родителей.) Модифицированное дерево доказательства, в корневой вершине которого находится ответное утверждение, изобра- жено на рис. 7.7. чмв Гл.
7. сзрименения исчисления аредикатав к решению задач В данном случае мы получаем довольно трудно интерпретируемое утверждение Р(р(а), а), содержащее сколемову функцию а. Интерпретация должна говорить о том, что независимо от сколемовой функции а, которая должна бы «нарушить» справедливость предположения, мы можем, как оказалось, доказать .Р(р(а), а). Иными словами, любой индивид, для которого предположение могло быть неверным, на самом деле удовлетворяет предположению.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
