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