Правила логического вывода для кванторов
Начнем с кванторов всеобщности. Предположим, что база знаний содержит следующую стандартную аксиому, которая передает мысль, содержащуюся во многих сказках, что все жадные короли — злые:
Vx King(x) л Greedy (х) Evil(x)
В таком случае представляется вполне допустимым вывести из нее любое из следующих высказываний:
King(John) A Greedy(John) Evil (John) King(Richard) A Greedy(Richard) Evil(Richard)
King(Father(John)) A Greedy(Father(John)) => Evil(Father(John))
Согласно правилу конкретизации высказывания с квантором всеобщности
(сокращенно UI — Universal Instantiation), мы можем вывести логическим путем любое высказывание, полученное в результате подстановки базового терма (терма без переменных) вместо переменной, на которую распространяется квантор всеобщности1. Чтобы записать это правило логического вывода формально, воспользуемся понятием подстановки, введенным в разделе 8.3. Допустим, что Subst(0,cc) обозначает результат применения подстановки 0 к высказыванию ос. В таком случае данное правило для любой переменной v и базового терма д можно записать следующим образом:
Например, три высказывания, приведенные выше, получены с помощью подстановок {x/John}, {х/Richard) и {х/ Father (John) }.
Соответствующее правило конкретизации высказывания с квантором существования (Existential Instantiation — EI) для квантора существования является немного более сложным. Для любых высказывания ос, переменной v и константного символа к, который не появляется где-либо в базе знаний, имеет место следующее:
3v а
Subst({v/k} ,а)
Например, из высказывания
Зх Crown (х) л OnHead(x, John) можно вывести высказывание
Crown (Ci) л OnHead (С±, John)
при условии, что константный символ Ci не появляется где-либо в базе знаний. По сути, в этом высказывании с квантором существования указано, что существует некоторый объект, удовлетворяющий определенному условию, а в процессе конкретизации просто присваивается имя этому объекту. Естественно, что это имя не должно уже принадлежать другому объекту. В математике есть прекрасный пример: предположим, мы открыли, что имеется некоторое число, которое немного больше чем 2,71828 и которое удовлетворяет уравнению d(xy) /dy=xy для х. Этому числу можно присвоить новое имя, такое как е, но было бы ошибкой присваивать ему имя существующего объекта, допустим, ТЕ. В логике такое новое имя называется сколемовской константой. Конкретизация высказывания с квантором существования — это частный случай более общего процесса, называемого сколемизацией, который рассматривается в разделе 9.5.
Конкретизация высказывания с квантором существования не только сложнее, чем конкретизация высказывания с квантором всеобщности, но и играет в логическом выводе немного иную роль. Конкретизация высказывания с квантором всеобщности может применяться много раз для получения многих разных заключений, а конкретизация высказывания с квантором существования может применяться только один раз, а затем соответствующее высказывание с квантором существования может быть отброшено. Например, после того как в базу знаний будет добавлено высказывание Kill (Murderer, Victim), становится больше не нужным высказывание Зх Kill (х, Victim). Строго говоря, новая база знаний логически не эквивалентна старой, но можно показать, что она эквивалентна с точки зрения логического вывода, в том смысле, что она выполнима тогда и только тогда, когда выполнима первоначальная база знаний.