Искусственный интеллект. Современный подход

Полнота резолюции

В настоящем разделе приведено доказательство полноты резолюции. Это доказательство может пропустить без ущерба для дальнейшего понимания текста любой читатель, который готов принять его на веру.
Мы покажем, что резолюция обеспечивает полноту опровержения (refutation completeness), а это означает, что если множество высказываний является невыполнимым, то резолюция всегда позволяет прийти к противоречию. Резолюцию нельзя использовать для выработки всех логических следствий из множества высказываний, но она может применяться для подтверждения того, что данное конкретное высказывание следует из множества высказываний. Поэтому резолюция может служить для поиска всех ответов на данный конкретный вопрос с помощью метода отрицаемой цели, который был описан выше в настоящей главе.
Примем как истинное такое утверждение, что любое высказывание в логике первого порядка (без использования равенства) может быть перезаписано в виде множества выражений в форме CNF. Это можно доказать по индукции на основе анализа формы высказывания, применяя в качестве базового случая атомарные высказывания [336]. Поэтому наша цель состоит в том, чтобы доказать следующее: если S— невыполнимое множество выражений, то применение к S конечного количества этапов резолюции приведет к противоречию.
Схема нашего доказательства повторяет первоначальное доказательство, приведенное Робинсоном, с некоторыми упрощениями, которые были внесены Гене-зеретом и Нильссоном [537]. Основная структура этого доказательства показана на рис. 9.9; оно осуществляется, как описано ниже.
Теорема Эрбрана
1. Вначале отметим, что если множество выражений S невыполнимо, то существует такое конкретное множество базовых экземпляров выражений 5, что это множество также невыполнимо (теорема Эрбрана).
ТЕОРЕМА ГЁДЕЛЯ О НЕПОЛНОТЕ
Немного дополнив язык логики первого порядка для обеспечения возможности применять схему математической индукции в арифметике, Гёдель сумел показать в своей теореме о неполноте, что существуют истинные арифметические высказывания, которые не могут быть доказаны.
Полное доказательство этой теоремы о неполноте немного выходит за рамки настоящей книги, поскольку в своем непосредственном виде оно занимает не меньше 30 страниц, но мы здесь приведем его набросок. Начнем с логической теории чисел. В этой теории существует единственная константа, 0, и единственная функция, 5 (функция определения преемника). В намеченной модели интерпретации этой теории 5(0) обозначает 1, 5(5(0) ) обозначает 2 и т.д., поэтому в рассматриваемом языке имеются имена для всех натуральных чисел. Кроме того, словарь языка включает функциональные символы +, х и Expt (возведение в степень), а также обычное множество логических связок и кванторов. Прежде всего, следует отметить, что множество высказываний, которые могут быть записаны на этом языке, может быть пронумеровано. (Для этого достаточно представить себе, что определен алфавитный порядок символов, а затем в алфавитном порядке расположено каждое из множеств высказываний с длиной 1, 2 и т.д.) Затем можно обозначить каждое высказывание а уникальным натуральным числом #а (которое называется гёделевским номером). Это — самый важный момент доказательства; в нем утверждается, что теория чисел включает отдельное имя для каждого из ее собственных высказываний. Аналогичным образом, с помощью гёделевского номера G(P) можно пронумеровать каждое возможное доказательство Р, поскольку любое доказательство — это просто конечная последовательность высказываний.
Теперь предположим, что имеется рекурсивно перечислимое множество А высказываний, которые представляют собой истинные утверждения о натуральных числах. Напомним, что высказывания из множества А можно именовать с помощью заданного множества целых чисел, поэтому можно представить себе, что на нашем языке записывается высказывание а (j, А) такого рода:
• Vi i — не гёделевский номер доказательства высказывания, гёделевским номером которого является j, где в доказательстве используются только предпосылки из множества А.
2. Затем прибегнем к базовой теореме резолюции (ground resolution theorem), приведенной в главе 7, в которой утверждается, что пропозициональная резолюция является полной для базовых высказываний.
3. После этого воспользуемся леммой поднятия, чтобы показать, что для любого доказательства по методу пропозициональной резолюции, в котором применяется множество базовых высказываний, существует соответствующее доказательство по методу резолюции первого порядка с использованием высказываний в логике первого порядка, из которых были получены базовые высказывания.
Затем допустим, что а представляет собой высказывание ос (#а. А), т.е. высказывание, в котором утверждается его собственная недоказуемость из А. (Утверждение о том, что такое высказывание всегда существует, является истинным, но его нельзя назвать полностью очевидным.)
Теперь применим следующий остроумный довод: предположим, что высказывание а доказуемо из А; в таком случае высказывание а ложно (поскольку в высказывании а утверждается, что оно не может быть доказано). Но это означает, что имеется некоторое ложное высказывание, которое доказуемо из А, поэтому А не может состоять только из истинных высказываний, а это противоречит нашей предпосылке. Поэтому высказывание а не доказуемо из А. Но именно это и утверждает о самом себе высказывание а, а это означает, что с — истинное высказывание.
Для того чтобы выполнить первый этап доказательства, нам потребуются три новых понятия, описанных ниже.
• Универсум Эрбрана. Если S— множество выражений, то Я5, универсум Эр-брана для множества 5, представляет собой множество всех базовых термов, которые могут быть сформированы из следующего:
а) функциональные символы из множества 5, если они имеются;
б) константные символы из множества 5, если они имеются; если они от-
сутствуют, то константный символ А.
Например, если множество S содержит только выражение -Р(х, F{x, А) ) v -iQ(х, A) v R(x, В), то Hs представляет собой следующее бесконечное множество базовых термов:
{A,BIF{AIA),F{A,B),F(BIA)IF{BIB),F{AIF{AIA))I...}
• Насыщение. Если S— множество выражений, а Р— множество базовых термов, то Р (S), насыщение S по отношению к р, представляет собой множество всех базовых выражений, полученное путем применения всех возможных совместимых подстановок базовых термов из Р вместо переменных в S.
• База Эрбрана. Насыщение множества выражений S по отношению к его универсуму Эрбрана называется базой Эрбрана множества S и записывается как HS{S). Например, если S содержит только приведенное выше выражение, то HS(S) представляет собой следующее бесконечное множество выражений:
Итак, мы доказали (и сэкономили 29 с половиной страниц), что для любого множества истинных высказываний теории чисел и, в частности, для любого множества базовых аксиом существуют другие истинные высказывания, которые не могут быть доказаны из этих аксиом. Из этого, кроме всего прочего, следует, что мы никогда не сможем доказать все теоремы математики в пределах любой конкретной системы аксиом. Очевидно, что это открытие имело для математики очень важное значение. Значимость этого открытия для искусственного интеллекта была предметом широких обсуждений, начиная с размышлений самого Гёделя. Мы вступим в эти дебаты в главе 26.
{—iP{A, F{A, A) ) v -i0(A,A) v R(A,B),
-iP(B,F(B, A) ) v -i0(B,A) v i?(B,B),
-iP(F(A, A) ,F(F(A,A) , A) ) v -iЈ (F (A, A) , A) v i?(F(A,A),B),
-iP(F(A,B),F(F(A,B),A)) v -iQ(F(A,B) ,A) v Ј(F(A,B),B), ...}
Эти определения позволяют сформулировать одну из форм теоремы Эрбрана [650]:
Если множество выражений S является невыполнимым, то существует конечное подмножество Hs (S), которое также является невыполнимым.
Допустим, что S* — конечное подмножество базовых высказываний. Теперь можно прибегнуть к базовой теореме резолюции (с. 311), чтобы показать, что резо-люционное замыкание RC{S' ) содержит пустое выражение. Это означает, что доведение до конца процесса пропозициональной резолюции применительно к S' приводит к противоречию.
Теперь, после определения того, что всегда существует доказательство по методу резолюции, в котором применяется некоторое конечное подмножество базы Эрбрана множества 5, на следующем этапе необходимо показать, что существует доказательство по методу резолюции, в котором используются выражения из самого множества S, которые не обязательно являются базовыми выражениями. Начнем с рассмотрения одного приложения правила резолюции. Из базовой леммы Робинсона следует приведенный ниже факт.
Допустим, что Ci и с2 — два выражения без общих переменных, a Ci' и с2' — базовые экземпляры d и С2. Если с1 — резольвента d ' и с2', то существует выражение с, такое, что, во-первых, С — резольвента Ci и с2, и, во-вторых, С — базовый экземпляр с.
Это утверждение называется клеммой поднятия (lifting lemma), поскольку оно позволяет поднять любой этап доказательства от базовых выражений к общим выражениям в логике первого порядка. Для того чтобы доказать свою основную лемму поднятия, Робинсону пришлось изобрести унификацию и определить все свойства наиболее общих унификаторов. Мы здесь не будем повторять доказательство Робинсона, а просто проиллюстрируем применение этой леммы следующим образом:
Ci = —\Р{х, F{x, А) ) v -nQ{x,A) v R{x,B) С2 = -iN(G(y) , z) v Р(Н(у) , z)
Ci' = -пР(Я(В) ,F{H(B) ,A)) V -nQ{H{B),A) V R{H{B),B) C2' = N{G{B) , F(H{B) ,A) ) V P(H(B) ,F(H(B) , A) ) С = -nN{G{B) , F(H(B) ,A) ) v-nQ(H(B),A) vR(H(B),B) С = -,N(G(y) ,F(H(y) ,A)) v -iQ(H{y),A) v R(H(y)tB)
Очевидно, что С* — действительно базовый экземпляр выражения С. Вообще говоря, для того чтобы выражения С± • и С2 * имели какие-либо резольвенты, они должны быть получены путем предварительного применения к выражениям Сг и С2 наиболее общего унификатора для пары взаимно дополнительных литералов в d и С2. Из леммы поднятия можно легко получить аналогичное, приведенное ниже утверждение о любой последовательности применений правила резолюции.
Для любого выражения С в резолюционном замыкании множества выражений S' существует выражение С в резолюционном замыкании множества выражений S, такое, что С — базовый экземпляр выражения с и логический вывод с имеет такую же длину, как и логический вывод с1.
Из этого факта следует, что если в резолюционном замыкании множества выражений ?" появляется пустое выражение, оно должно также появиться в резолюционном замыкании множества выражений S. Это связано с тем, что пустое выражение не может быть базовым экземпляром любого другого выражения. Подведем итог: мы показали, что если множество выражений S невыполнимо, то для него существует конечная процедура логического вывода пустого выражения с помощью правила резолюции.
Поднятие способа доказательства теорем от базовых выражений к выражениям первого порядка обеспечивает огромное увеличение мощи доказательства. Это увеличение связано с тем фактом, что теперь в доказательстве первого порядка конкретизация переменных может выполняться только по мере того, как это потребуется для самого доказательства, тогда как в методах с использованием базовых выражений приходилось исследовать огромное количество произвольных конкретизации.