Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 111
Текст из файла (страница 111)
После этого воспользуемся леммой поднятия, чтобы показать, что для любого доказательства по методу пропозициональной резолюции, в котором применяется множество базовых высказываний, существует соответствующее доказательство по методу резолюции первого порядка с использованием высказываний в логике первого порядка, из которых были получены базовые высказывания. ТЕОРЕМА ГЕДЕЛЯ О НЕПОЛНОТЕ Немного дополнив язык логики первого порядка для обеспечения возможности применять схему математической ицдукции в арифметике, Гедель сумел показать в своей теореме о неполноте, что существуют истинные арифметические высказывания, которые не могут быть доказаны.
Полное доказательство этой теоремы о неполноте немного выходит за рамки настоящей книги, поскольку в своем непосредственном виде оно занимает не меньше 30 страниц, но мы здесь приведем его набросок. Начнем с логической теории чисел. В этой теории существует единственная константа, О, и единственная функция, 8 (функция определения преемника). В намеченной модели интерпретации этой теории Я(0) обозначает 1, Я(Я(0) ) обозначает 2 и т.д., поэтому в рассматриваемом языке имеются имена для всех натуральных чисел. Кроме того, словарь языка включает функциональные символы +, х и дхрс (возведение в степень), а также обычное множество логических связок и кванторов.
Прежде всего, следует отметить, что множество высказываний, которые могут быть записаны на этом языке, может быть пронумеровано. (Для этого достаточно представить себе, что определен алфавитный порядок символов, а затем в алфавитном порядке расположено каждое из множеств высказываний с длиной 1, 2 и т.д.) Затем можно обозначить каждое высказывание а уникальным натуральным числом Фа (которое называется геделевским номером). Это — самый важный момент доказательства; в нем утверждается, что теория чисел включает отлельное имя для каждого из ее собственных высказываний.
Аналогичным образом, с помощью геделевского номера О(Р) можно пронумеровать каждое возможное доказательство Р, поскольку любое доказательство — это просто конечная последовательность высказываний. Теперь предположим, что имеется рекурсивно перечислимое множество А высказываний, которые представляют собой истинные утверждения о натуральных числах. Напомним, что высказывания из множества А можно именовать с помощью заданного множества целых чисел, поэтому можно представить себе, что на нашем языке записывается высказывание а(7', л) такого рода: ° ЧЗ з — не геделевский номер доказательства высказывания, геделевским номером которого является 3', где в доказательстве используются только предпосылки из множества л.
418 Часть Н1. Знания и рассуждения Затем допустим, что о предсташгяет собой высказывание а ( ()а, А), т.е. высказывание, в котором утверждается его собственная недоказуемость из А. (Утверждение о том, что такое высказывание всегда существует, является истинным, но его нельзя назвать полностью очевидным.) Теперь применим следующий остроумный довод: предположим, что высказывание о доказуемо из А; в таком случае высказывание о ложно (поскольку в высказывании о утверждается, что оно не может быть доказано).
Но это означает, что имеется некоторое ложное высказывание, которое доказуемо из А, поэтому А не может состоять только из истинных высказываний, а это противоречит нашей предпосылке. Поэтому высказывание о не доказуемо из А. Но именно это и утвержлает о самом себе высказывание а, а это означает, что о — истинное высказывание. Итак, мы доказали (и сэкономили 29 с половиной страниц), что для любого множества истинных высказываний теории чисел и, в частности, для любого множества базовых аксиом существуют лругие истинные высказывания, которые не могут быть доказаны из этих аксиом. Из этого, кроме всего прочего, следует, что мы никогда не сможем доказать все теоремы математики в пределах любой конкретной системы аксиом.
Очевидно, что это открытие имело для математики очень важное значение. Значимость этого открытия для искусственного интеллекта была предметом широких обсуждений, начиная с размышлений самого Геделя. Мы вступим в эти дебаты в главе 26. Для того чтобы выполнить первый этап доказательства, нам потребуются три новых понятия, описанных ниже. ° 'в. Универсум Эрбрана. Если  — множество выражений, то В„универсум Эрбрана для множества Я, представляет собой множество всех базовых термов, которые могут быть сформированы из следующего: а) функциональные символы из множества Я, если они имеются; б) константные символы из множества В, если они имеются; если они отсутствуют, то константный символ А.
Например, если множество В содержит только выражение - Р(х, В(х, А) ) 2(х, А) м В(х, в), то н, представляет собой следующее бесконечное множество базовых термов: (А, В, Р(А, А), Р(А, В), В(В, А), Р(В, В), Р(А,В(А, А) ),...) ° 'в. Насыщение. Если Я вЂ” множество выражений, а  — множество базовых термов, то р(я, насыщение я по отношению к В, представляет собой множество всех базовых выражений, полученное путем применения всех возможных совместимых подстановок базовых термов из р вместо переменных в я. ° 'в. База Эрбраиа.
Насыщение множества выражений В по отношению к его универсуму Эрбрана называется базой Эрбрана множества Я и записывается как В, ( Я) . Например, если Я содержит только приведенное выше выражение, то Н,(В) представляет собой следующее бесконечное множество выражений; Глава 9. Логический вывод в логике первого порядка 419 ( Р(А, Р(А, А) ) ч Сг(А,А) ч к(А, В), Р(В,Р(В,А) ) ч ()(В,А) ч К(В,В), — Р(Р(А, А), Р(Р(А,А),А) ) ч гС(Р(А,А),А) ч Н(Р(А,А),В), — Р(Р(А, В), Р(Р(А, В),А) ) ч гС(Р(А,В),А) ч Н(Р(А, В), В), Эти определения позволяют сформулировать одну из форм 'в.
теоремы Эрбрана 1650): Если множество выражений В является невыполнимым, то существует конечное подмножество и, ( н), которое также является невыполнимым. Допустим, что Я' — конечное подмножество базовых высказываний. Теперь можно прибегнуть к базовой теореме резолюции (с. 311), чтобы показать, что резолюцнонное замыкание нс( и' ) содержит пустое выражение. Это означает, что доведение до конца процесса пропозиционзльной резолюции применительно к Я' приводит к противоречию. Теперь, после определения того, что всегда существует доказательство по методу резолюции, в котором применяется некоторое конечное подмножество базы Эрбрана множества Н, на следующем этапе необходимо показать, что существует доказательство по л(етоду резолюции, в котором используются выражения из самого множества В, которые не обязательно являются базовыми выражениями.
Начнем с рассмотрения одного приложения правила резолюции. Из базовой леммы Робинсона следует приведенный ниже факт. ДопУстим, что с; и сг — два выРажсниа бсз общих пеРсмснных, а сг ' и сг ' — базовые эк- ЗЕМЛЛярЫ С, И Сг. ЕСЛИ С' — рСЗОЛЫгСНта С, ' я С,', тс СуШЕСтауст ВЫражЕННС С, таКОЕ, что, во-первых, с — резольвснта сг и сг, и, во-вторых, с' — базовый экземпляр с. Это утверждение называется ск леммой поднятия (!(й(шй !епппа), поскольку оно позволяет поднять любой этап доказательства от базовых выражений к общим выражениям в логике первого порядка. Для того чтобы доказать свою основную лемму поднятия, Робинсону пришлось изобрести унификацию и определить все свойства наиболее общих унцфикаторов.
Мы здесь не будем повторять доказательство Робки(- сона, а просто проиллюстрнруем применение этой леммы следующим образом: Сг = Р(х,у(х,А)) ч С(х,А) ч Н(х,В) С, = -.Н(О(у),х) ч Р(Н(у),х) Сг' = Р(Н(В), Р(Н(В),А) ) ч — Ц(Н(В), А) ч Н (Н(В), В) Сг' = Н(0(В),Р(Н(В), А) ) ч Р(Н(В), Р(Н(В), А) ) С' = Н(а(В),Р(Н(В), А) ) ч †,д(Н(В), А) ч К(Н(В), В) С = М(О(у), Р(Н(у), А) ) ч — О(Н(у), А) ч Я(Н(у), В) Очевидно, что С' — действительно базовый экземпляр выражения С.
Вообще говоря, для того чтобы выражения С,' и С, ' имели какие-либо резольвенты, они должны быть получены путем предварительного применения к выражениям С, и С, наиболее общего унификатора для пары взаимно дополнительных литералов в С, и С,. Из леммы поднятия можно легко получить аналогичное, приведенное ниже утверждение о любой последовательности применений правила резолюции. Для любого выражения с' в революционном замыкании множества выражений н' существует выражение с в революционном замыкании множества выражений В, такое, что с' — базовый экземпляр выражения с и логический вывод с имеет такую же длину, как и логический вывод с' . 420 Часть П1.
Знания и рассуждения Из этого факта следует, что если в резолюционном замыкании множества выражений Я' появляется пустое выражение, оно должно также появиться в резолюционном замыкании множества выражений д. Это связано с тем, что пустое выражение не может быть базовым экземпляром любого другого выражения.
Подведем итог: мы показали, что если множество выражений Я невыполнимо, то для него существует конечная процедура логического вывода пустого выражения с помощью правила резолюции. Поднятие способа доказательства теорем от базовых выражений к выражениям первого порядка обеспечивает огромное увеличение мощи доказательства. Это увеличение связано с тем фактом, что теперь в доказательстве первого порядка конкретизация переменных может выполняться только по мере того, как это потребуется для самого доказательства, тогда как в методах с использованием базовых выражений приходилось исследовать огромное количество произвольных конкретизаций.
Учет отношения равенства Ни в одном из методов логического вывода, описанных до сих пор в этой главе, пе учитывалось отношение равенства. Для решения этой задачи может быть принято три различных подхода. Первый подход состоит в аксиоматизации равенства— включении в базу знаний высказываний, касающихся отношения равенства.
При этом необходимо описать, что отношение равенства является рефлексивным, симметричным и транзитивным, а также сформулировать утверждение, что мы можем в любом предикате или функции заменять равные литералы равными. Таким образом, требуются три базовые аксиомы и еще по одной аксиоме для каждого предиката и функции, как показано ниже. )гх х = х )гхух=у~у=х )(хухх=улу=х~х ()х,у х = у .=» (у»(х)»» д»(у) ) ((х,у х = у =» (гя(х)»» Р»(у)) )(ь,х,у,а и = у л х = х ~ (Г1(ь',х) = у»(у,х)) )(»»,х,у,е и = у л х = х ~ (72(ь',х) = »»(у е)) При наличии в базе знаний таких высказываний любая стандартная процедура логического вывода, такая как резолюция, позволяет решать задачи, требующие формирования рассуждений с учетом отношения равенства, например находить решения математических уравнений.
Еще один способ учета отношения равенства состоит в использовании дополнительного правила логического вывода. В простейшем правиле, правиле демодуляции, берется единичное выражение х=у, после чего терм у подставляется вместо любого герма, который унифицируется с термом х в каком-то другом выражении. Более формально эту идею можно представить, как описано ниже. ° Ъ Демодуляция.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
