Главная arrow Логика arrow Правила для кванторов
Как начинался компьютер
Компьютерная революция
Двоичный код
Разработки военных лет
Интегральные микросхемы
Микрокомпьютер
Персоны
Сеть
Язык компьютера
Развитие ПО
Гибкие системы
Средства разработки
Информатика
Вычислительная наука
Операционные системы
Искусственный интеллект
Предыстория
Поиск
Знания и рассуждения
Логика
Робототехника
 

 
Правила для кванторов Печать

Начнем с кванторов всеобщности. Предположим, что база знаний содержит следующую стандартную аксиому, которая передает мысль, содержащуюся во многих сказках, что все жадные короли — злые:

Vx King(x) л Greedy(x) => Evil(x)

В таком случае представляется вполне допустимым вывести из нее любое из следующих высказываний:

King {John) л Greedy {John) :=> Evil {John)

King{Richard) л Greedy{Richard) => Evil{Richard)

King{Father{John)) л Greedy{Father{John)) => Evil{Father{John))

Согласно правилу конкретизации высказывания с квантором всеобщности (сокращенно UIUniversal Instantiation), мы можем вывести логическим путем любое высказывание, полученное в результате подстановки базового терма (терма без переменных) вместо переменной, на которую распространяется квантор всеобщности. Чтобы записать это правило логического вывода формально, воспользуемся понятием подстановки, введенным в разделе 8.3. Допустим, что Subst@,cc) обозначает результат применения подстановки 0 к высказыванию ос. Например, три высказывания, приведенные выше, получены с помощью подстановок {x/John}, {х/Richard] и {х/ Father {John) }.

Соответствующее правило конкретизации высказывания с квантором существования (Existential Instantiation — EI) для квантора существования является немного более сложным. Для любых высказывания ос, переменной v и константного символа к, который не появляется где-либо в базе знаний, имеет место следующее: Зх Crown (х) л OnHead{x, John) можно вывести высказывание Crown ( Ci) л OnHead {d , John) при условии, что константный символ Ci не появляется где-либо в базе знаний.

По сути, в этом высказывании с квантором существования указано, что существует некоторый объект, удовлетворяющий определенному условию, а в процессе конкретизации просто присваивается имя этому объекту. Естественно, что это имя не должно уже принадлежать другому объекту. В математике есть прекрасный пример: предположим, мы открыли, что имеется некоторое число, которое немного больше чем 2,71828 и которое удовлетворяет уравнению d(xy) /dy=xy для х.

Этому числу можно присвоить новое имя, такое как е, но было бы ошибкой присваивать ему имя существующего объекта, допустим, те. В логике такое новое имя называется сколемовской константой. Конкретизация высказывания с квантором существования — это частный случай более общего процесса, называемого сколемизацией, который рассматривается в предыдущем разделе.

Конкретизация высказывания с квантором существования не только сложнее, чем конкретизация высказывания с квантором всеобщности, но и играет в логическом выводе немного иную роль. Конкретизация высказывания с квантором всеобщности может применяться много раз для получения многих разных заключений, а конкретизация высказывания с квантором существования может применяться только один раз, а затем соответствующее высказывание с квантором существования может быть отброшено. Например, после того как в базу знаний будет добавлено высказывание Kill {Murderer, Victim), становится больше не нужным высказывание Зх Kill {х, Victim). Строго говоря, новая база знаний логически не эквивалентна старой, но можно показать, что она эквивалентна с точки зрения логического вывода, в том смысле, что она выполнима тогда и только тогда, когда выполнима первоначальная база знаний.

 

Приведение к пропозициональному логическому выводу

Получив в свое распоряжение правила вывода высказываний с кванторами из высказываний без кванторов, мы получаем возможность привести вывод в логике первого порядка к выводу в пропозициональной логике. В данном разделе будут изложены основные идеи этого процесса, а более подробные сведения приведены в предыдущем разделе.

Основная идея состоит в следующем: по аналогии с тем, как высказывание с квантором существования может быть заменено одной конкретизацией, высказывание с квантором всеобщности может быть заменено множеством всех возможных конкретизации. Например, предположим, что наша база знаний содержит только такие высказывания:

Vx King(x) л Greedy(x) => Evil{x)

King{John)

Greedy {John)

Brоther(Richard,John)

Затем применим правило конкретизации высказывания с квантором всеобщности к первому высказыванию, используя все возможные подстановки базовых термов из словаря этой базы знаний— в данном случае {х/John} и {х/Richard]. Мы получим следующие высказывания:

King(John) л Greedy{John) => Evil{John)

King{Richard) a Greedy{Richard) => Evil{Richard)

и отбросим высказывание с квантором всеобщности. Теперь база знаний становится по сути пропозициональной, если базовые атомарные высказывания (King {John), Greedy {John) и т.д.) рассматриваются как пропозициональные символы. Поэтому теперь можно применить любой из алгоритмов полного пропозиционального вывода для получения таких заключений, как Evil (John).

Как показано в предыдущем разделе, такой метод пропозиционализации (преобразования в высказывания пропозициональной логики) может стать полностью обобщенным; это означает, что любую базу знаний и любой запрос в логике первого порядка можно пропозиционализировать таким образом, чтобы сохранялось логическое следствие. Таким образом, имеется полная процедура принятия решения в отношении того, сохраняется ли логическое следствие... или, возможно, такой процедуры нет.

Дело в том, что существует такая проблема: если база знаний включает функциональный символ, то множество возможных подстановок базовых термов становится бесконечным! Например, если в базе знаний упоминается символ Father, то существует возможность сформировать бесконечно большое количество вложенных термов, таких как Father {Father {Father {John) ) ). А применяемые нами пропозициональные алгоритмы сталкиваются с затруднениями при обработке бесконечно большого множества высказываний.

К счастью, имеется знаменитая теорема, предложенная Жаком Эрбраном, согласно которой, если некоторое высказывание следует из первоначальной базы знаний в логике первого порядка, то существует доказательство, которое включает лишь конечное подмножество этой пропозиционализированной базы знаний. Поскольку любое такое подмножество имеет максимальную глубину вложения среди его базовых термов, это подмножество можно найти, формируя вначале все конкретизации с константными символами (Richard и John), затем все термы с глубиной 1 (Father (Richard) и Father (John)), после этого все термы с глубиной 2 и т.д. до тех пор, пока мы не сможем больше составить пропозициональное доказательство высказывания, которое следует из базы знаний.

Выше был кратко описан один из подходов к организации вывода в логике первого порядка с помощью пропозиционализации, который является полным, т.е. позволяет доказать любое высказывание, которое следует из базы знаний. Это — важное достижение, если учесть, что пространство возможных моделей является бесконечным. С другой стороны, до тех пор пока это доказательство не составлено, мы не знаем, следует ли данное высказывание из базы знаний! Что произойдет, если это высказывание из нее не следует? Можем ли мы это определить? Как оказалось, для логики первого порядка это действительно невозможно.

Наша процедура доказательства может продолжаться и продолжаться, вырабатывая все более и более глубоко вложенные термы, а мы не будем знать, вошла ли она в безнадежный цикл или до получения доказательства остался только один шаг. Такая проблема весьма напоминает проблему останова машин Тьюринга. Алан Тьюринг и Алонсо Черч доказали неизбежность такого состояния дел, хотя и весьма различными способами.