Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 109
Текст из файла (страница 109)
В этом разделе будет показано, как распространить резолюцию на логику первого порядка. Проблема существования полных процедур доказательства всегда является предметом непосредственного внимания математиков. Если бы удалось найти полную процедуру доказательства для математических утверждений, это повлекло бы за собой два последствия: во-первых, вывод всех заключений мог бы осуществляться механически; во-вторых, всю математику можно было бы построить как логическое следствие некоторого множества фундаментальных аксиом. Поэтому вопрос о полноте доказательства стал в ХХ веке предметом наиболее важных математических работ.
В 1930 году немецкий математик Курт Гедель доказал первую 'гя теорему о полноте для логики первого порядка, согласно которой любое высказывание, являющееся следствием заданных аксиом, имеет конечное доказательство. (Но никакая действительно применимая на практике процедура доказательства не была найдена до тех пор, пока Дж.Э. Робинсон не опубликовал в 1965 году алгоритм резолюции.) В 1931 году Гелель доказал еше более знаменитую 'в. теорему о неполноте. В этой теореме утверждается, что любая логическая система, которая включает принцип индукции (а без этого принципа удается построить лишь очень малую часть дискретной математики), обязательно является неполной. Поэтому сушествуют такие высказывания, которые следуют из заданных аксиом, но в рамках данной логиче- 4]0 Часть! П.
Знания и рассуждения ской системы для них невозможно найти конечное доказательство. Иголка действительно может быть в метафорическом стоге сена, но ни одна процедура не позволяет гарантировать, что она будет найдена. Несмотря на то, что теорема Геделя о неполноте устанавливает определенные пределы, программы автоматического доказательства теорем на основе резолюции широко применялись и применяются для обоснования математических теорем, включая несколько таких теорем, для которых до сих пор не было известно доказательство.
Кроме того, программы автоматического доказательства теорем успешно использовались для проверки проектов аппаратных средств, формирования логически правильных программ, а также во многих других приложениях. Конъюнктивная нормальная форма для логики первого порядка Как и в случае пропозициональной логики, для резолюции в логике первого порядка требуется, чтобы высказывания находились в конъюнктивной нормальной форме [Соп]цпс()че Хоста] Ропп — СХГ), т.е. представляли собой конъюнкцию выражений, в которой каждое выражение представляет собой дизъюнкцию литералов'. Литералы могут содержать переменные, на которые, согласно принятому предположению, распространяется квантор всеобщности.
Например, высказывание Чх Лгпег1сап(х) л Меароп(у) л Яе11в(х,у, е) л НоеС11е(г) ~ Сгзтхпа1(х) принимает в форме СХГ следующий вид: — гилес1сап(х) ч (уеароп(у)ч Яе11е(х,у, г) ч ноес11е(г) ч сгут1па1(х) Каждое высказывание в логике первого порядка может быть преобразовано в эквивалентное с точки зрения логического вывода высказывание СЛЖ В частности, высказывание СМГ является невыполнимым тогда и только тогда, когда невыполнимо первоначальное высказывание, поэтому мы получаем основу для формирования доказательств от противного с помощью высказываний С]ч]Г. Процедура преобразования любого высказывания в форму СМГ весьма подобна процедуре, применяемой в пропозициональной логике, которая показана на с.
308. Принципиальное различие связано с необходимостью устранения кванторов существования. Проиллюстрируем эту процедуру на примере преобразования в форму СМГ высказывания "Каждого, кто любит всех животных, кто-то любит", или 1(х [1(у Ап1зла1(у) ~ ьочев(х,у) ] => [Зу 1очез(у,х) ] Ниже приведены этапы этого преобразования. ° Устранение импликаций: )Ух [-~Чу Лп1та1(у) ч лосев(х,у)) ч [Зу Ьочев(у,х)] ° Перемещение связок - внутрь выражений. Кроме обычных правил для отрицаемых связок, нам нужны правила для отрицаемых кванторов. Поэтому получаем следующие правила: ь Как показано в упр.
7.!2, любое выражение может быть представлено как имлликация с конъюнкцией атомов слева и дизъюнкцией атомов справа. Эта форма, иногда называемая формой Ковальского, прн использовании записи с символом импликации, ориентированным справа налево [851], часто бывает намного более удобной для чтения по сравнению с другими формамн. Глава 9. Логический вывод в логике первого порядка 411 Чх р принимает вид Вх лр Эх р принимает вид Чх -~р Рассматриваемое высказывание проходит через такие преобразования: цх [Ву — (-ч(пдта1(у) ч йочеа(х,у) ) ) ч [Ву ьоуев(у,х) ] чх [Ву Апдта1 (у) л — Ьочеа (х,у) ] ч [Ву ьочеа (у, х) ] чх Яу Апдта1(у) л — вечеа(х,у) ] ч Цу вечеа(у,х) ] Обратите внимание на то, что квантор всеобщности [Чу) в предпосылке импликации стал квантором существования.
Теперь это высказывание приобрело такое прочтение: "Либо существует какое-то животное, которого х не любит, либо [если это утверждение не является истинным) кто-то любит х". Очевидно, что смысл первоначального высказывания был сохранен. ° Стандартизация переменных. В высказываниях наподобие (Чх р(х) ) (Бх Ц(х) ), в которых дважды используется одно и то же имя переменной, изменим имя одной из переменных.
Это позволит в дальнейшем избежать путаницы после того, как будут удалены кванторы. Поэтому получим следующее: цх [Ву Апдта1(у) л вечеа(х,у) ] ч [Эг Ъочеа(г,х) ) ° Сколемизация. ъ. Сколемизация — это процесс устранения кванторов существования путем их удаления. В данном простом случае этот процесс подобен применению правила конкретизации с помощью квантора существования, приведенного в разделе 9.1: преобразовать Зх р(х) в р(А), где А — новая константа. Однако, если это правило будет непосредственно применено к высказыванию, рассматриваемому в качестве примера, то будет получено следующее высказывание: Чх (Апдта1(А) л Ьочеа(х,А) ] ч вечеа(п,х) которое имеет полностью неправильный смысл: в нем утверждается, что каждый либо не способен любить какое-то конкретное животное А, либо его любит некоторая конкретная сущность в.
В действительности первоначальное высказывание позволяет каждому человеку не быть способным любить какоето другое животное или быть любимым другим человеком. Поэтому желательно, чтобы сущности, определяемые в процессе сколемизации, зависели от х: )(х [Аптта1 (Е'(х) ) л йочеа (х, у(х) ) ) ч Ьоиеа (8(х), х) где р и о — 'ъ. сколемовские функции. Общее правило состоит в том, что все параметры сколемовской функции должны быть переменными, на которые распространяются кванторы всеобщности, в область действия которых попадает соответствующий квантор существования. Как и при использовании конкретизации с помощью квантора существования, сколемизированное высказывание является выполнимым тогда и только тогда, когда выполнимо первоначальное высказывание.
° Удаление кванторов всеобщности. В данный момент на все оставшиеся переменные должны распространяться кванторы всеобщности. Кроме того, данное высказывание эквивалентно тому, в котором все кванторы всеобщности перенесены влево. Поэтому кванторы всеобщности могут быть удалены следующим образом: Часть П1. Знания и рассуждения 412 (Апгта1(Е(х) ) л пьочея(х,к(х) ) ] ч Ьочея(О(х),х) ° Распределение связки ч пол: (Апзта1(Е(х)) ч Гокея(О(х),х)] л ( Ьочея(х,а(х)) ч йочея(О(х),х)1 На этом этапе может также потребоваться выполнить раскрытие скобок во вложенных конъюнкциях и дизьюнкциях.
Теперь рассматриваемое высказывание находится в форме С]ч'Г и состоит из двух выражений. Оно полностью недоступно для восприятия. (Помочь его понять может такое пояснение, что сколемовская функция Г(х) указывает на животное, которое потенциально может быть нелюбимым лицом х, а б(х) указывает на кого-то, кто может любить лицо х,) К счастью, людям редко приходится изучать высказывания в форме С]ч Г, поскольку показанный выше процесс преобразования может быть легко автоматизирован.
Прави.по логического вывода с помощью резолюции Правило резолюции для выражений в логике первого порядка представляет собой поднятую версию правила резолюции для пропозициональной логики, приведенного на с. 307. Два выражения, которые, согласно принятому предположению, должны быть стандартизированными таким образом, чтобы в них не было общих переменных, могут быть подвергнуты операции резолюции, если они содержат взаимно дополнительные литералы. Пропозициональные литералы являются взаимно дополнительными, если один из них представляет собой отрицание другого, а литералы в логике первого порядка являются взаимно дополнительными, если один из них унифицируется с отрицанием другого.
Поэтому имеет место следующее правило: ч...чГь,тгч...чт„ япцяе(0,1~ ч ...ч Г, г ч Гг г ч . ч 6. ч т; ч .. ч т „ч т„г ч ... ч т„) где()пьгу(г,, т,.) = 0. Например, можно применить операцию резолюции к следующим двум выражениям: (Апзта1(1 (х) ) ч Ьочея(О(х), х) 1 и ( Ьочея(и, ч) ч К111я(и, ч) ] путем устранения взаимно дополнительных литералов Ьочея(6(х), х) и ьочея(п, ч) с помощью унификатора 0 = (ц/0(х), ч/х] для получения следуюгцего выражения, называемого резольвентой: (Ап1та1 (а (х) ) ч К111я (О(х), х) ] Только что приведенное правило называется правилом Ъ. бинарной резолюции, поскольку в нем происходит удаление с помощью резолюции двух и только двух взаимно дополнительных литералов. Но правило бинарной резолюции, отдельно взятое, не позволяет получить полную процелуру логического вывода. С другой стороны, правило полной резолюции позволяет удалять в каждом выражении подмножества литералов, которые являются унифицируемыми.
Альтернативный подход состоит в том, чтобы распространить операцию факторизации (удаления избыточных литералов) на логику первого порялка. В пропозициональной факторизации два литерала сводятся к олному, если они являются идентичными, а в факторизации первого порядка два литерала сводятся к одному, если они являются унифицируемыми. 413 Глава 9. Логический вывод в логике первого порядка Унификатор должен быть применен ко всему выражению. Сочетание бинарной ре- золюции и факторизации позволяет создать полную процедуру логического вывода Примеры доказательств При использовании резолюции доказательство того, что кд 1 а (из базы знаний следует высказывание а) осуществляется путем доказательства невыполнимости выражения кв А -кх, т.е.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
