Семантика исчисления предикатов обеспечивает основу для формализации теории логического вывода (logical inference). Возможность логически выводить новые правильные выражения из набора истинных утверждений — это важное свойство исчисления предикатов. Логически выведенные выражения корректны, потому что они совместимы со всеми предыдущими интерпретациями первоначального набора выражений. Вначале обсудим вышесказанное неформально, а затем введем ряд определений для формализации этих утверждений.
Говорят, что интерпретация, которая делает предложение истинным, удовлетворяет этому предложению. Если интерпретация удовлетворяет каждому элементу набора выражений, то говорят, что она удовлетворяет набору. Выражение X логически следует из набора выражений S исчисления предикатов, если каждая интерпретация, которая удовлетворяет S, удовлетворяет и X. Это утверждение дает основание для проверки правильности правил вывода: функция логического вывода должна производить новые предложения, которые логически следуют из данного набора предложений исчисления предикатов.
Важно верно понимать значение слов логически следует: логическое следование выражения X из S означает, что оно должно быть истинным для каждой интерпретации, которая удовлетворяет первоначальному набору выражений S. Это означает, например, что любое новое выражение исчисления предикатов, добавленное к миру блоков на рис. 2.3, должно быть истинным в этом мире. Оно должно быть истинным и при любой другой интерпретации, которую мог бы иметь этот набор выражений.
Термин логически следует вовсе не означает, что X выведено из S, или что его можно вывести из S. Это просто означает, что X истинно для каждой интерпретации (потенциально до бесконечности), которая удовлетворяет S. Однако системы предикатов могут иметь бесконечное число возможных интерпретаций, поэтому практическая необходимость проверять все интерпретации возникает весьма редко. В вычислительном отношении правила вывода (inference rule) позволяют определять, когда выражение как компонент интерпретации логически следует из этой интерпретации.
Понятие логически следует обеспечивает формальное основание для доказательства разумности и правильности правил вывода[А.Д.12] .
Правило вывода обеспечивает создание новых предложений исчисления предикатов на основе данных предложений. Следовательно, правила вывода производят новые предложения, основанные на синтаксической форме данных логических утверждений. Если каждое предложение X, полученное с помощью некоторого правила вывода на множестве S логических выражений, также логически следует из S, то говорят, что это правило вывода обосновано (sound).
Если система правил вывода способна произвести каждое выражение, которое может логически следовать из S, то говорят, что эта система правил вывода является полной. Приведенное ниже правило modus ponens и принцип резолюции (resolution), представленный в главе 12, являются примерами обоснованных правил вывода, которые при использовании соответствующих стратегий полны. Логические системы вывода обычно используют обоснованные правила вывода, однако далее (в главах 5, 9, 10 и 14) мы рассмотрим эвристические рассуждения и рассуждения на основе здравого смысла, которые опускают это требование.
Формализуем эти мысли с помощью следующих определений.
ОПРЕДЕЛЕНИЕ
УДОВЛЕТВОРЯТЬ, МОДЕЛЬ, АДЕКВАТНОСТЬ
Для выражения X исчисления предикатов и интерпретации / имеют место следующие
определения.
Если X имеет значение Г на / при конкретных значениях переменных, то говорят, что
/ удовлетворяет X.
Если / удовлетворяет X при всех значениях переменных, то / является моделью X. X выполнимо (satisfiable) тогда и только тогда, когда существуют такая интерпретация и значение переменной, которые ему удовлетворяют; в противном случае X невыполнимо (unsatisfiable).
Набор выражений выполним тогда и только тогда, когда существуют интерпретация и значения переменных, которые удовлетворяют каждому элементу. Если набор выражений невыполним, то говорят, что он противоречив (inconsistent). Если X имеет значение Г для всех возможных интерпретаций, то говорят, что X имеет силу, или адекватно (valid).
В примере на рис. 2.3 мир блоков является моделью для логического описания. При этой интерпретации все предложения в примере были истинными. Если база знаний реализована как набор истинных утверждений для предметной области задачи, то предметная область служит моделью для базы знаний.
Выражение ЭХ (р(Х) л -.р(Х)) противоречиво, потому что оно не может быть удовлетворено ни при какой интерпретации или значениях переменных. С другой стороны, выражение VX (р(Х) v ->р(Х)) адекватно.
Для проверки адекватности выражений, не содержащих переменных, можно использовать метод таблиц истинности. Поскольку не всегда можно определить, адекватно ли выражение, содержащее переменные (как говорилось выше, процесс может не закончиться), говорят, что полное исчисление предикатов "неразрешимо". Однако существуют методы доказательства, которые позволяют генерировать любое выражение, логически следующее из данного набора выражений. Они называются процедурами полного доказательства (complete proof procedures[А.Д.13] ).
ОПРЕДЕЛЕНИЕ
ПРОЦЕДУРА ДОКАЗАТЕЛЬСТВА
Процедура доказательства (proof procedure) — это комбинация правил вывода и алгоритма применения этих правил к набору логических выражений для создания новых предложений.
В главе 11 представлены процедуры доказательства для правил резолюции (resolution inference rule).
Используя эти определения, можно формально определить термин "логически следует".
ОПРЕДЕЛЕНИЕ
ЛОГИЧЕСКИ СЛЕДУЕТ, ОБОСНОВАННЫЙ И ПОЛНЫЙ
Выражение исчисления предикатов X логически следует из набора S выражений исчисления предикатов, если каждая интерпретация и значения переменных, которые удовлетворяет S, удовлетворяют и X.
Правило вывода обосновано (sound), если каждое выражение исчисления предикатов, полученное в соответствии с правилом из множества S выражений исчисления предикатов, также логически следует из S.
Правило вывода полно (complete), если на данном множестве S выражений исчисления предикатов правило позволяет вывести любое вьфажение, которое логически следует из S.
Правило modus ponens (правило отделения, или модус поненс) — это обоснованное правило вывода. Если дано выражение вида Р—> О и другое выражение вида Р, и оба выражения истинны на интерпретации /, то modus ponens позволяет нам сделать вывод, что О тоже истинно на этой интерпретации. Действительно, поскольку modus ponens является обоснованным правилом, О истинно для всех интерпретаций, для которых Р и P^>Q являются истинными.
Определения правила modus ponens и ряда других полезных правил вывода даны ниже.
Если известно, что предложения Р и P->Q истинны, то модус поненс позволяет вывести О.
Согласно правилу вывода модус толленс (modus tollens), если известно, что Р—>0 является истинным и О ложно, можно вывести -,Р.
Исключение "И" — правило, позволяющее вывести истинность обоих конъюнктов на основе истинности конъюнктивного предложения. Например, если PaQ истинно, можно сделать вывод, что Р и О истинны.
Введение "И" позволяет вывести истинность конъюнкции из истинности ее конъюнктов. Например, если Р и О истинны, то конъюнкция PaQ истинна. Универсальное инстанцирование сводится к следующему: если любую переменную, стоящую под квантором всеобщности в истинном предложении, заменить любым соответствующим термом из области определения, то результирующее выражение — истинно. Таким образом, если а принадлежит той же области определения, что и X и VXр(Х), то можно вывести р(а[А.Д.14] ). В качестве простого примера применения правила модус поненс в исчислении высказываний рассмотрим следующие предложения: "если идет дождь, то земля будет влажной" и "идет дождь". Если Р обозначает "идет дождь" и О есть "земля, влажная", то первое выражение можно записать в виде P->Q. Поскольку действительно сейчас идет дождь (Р истинно), получаем систему аксиом.
P->Q Р
Применив правило модус поненс к набору истинных выражений, можно добавить тот факт, что земля является влажной О.
Правило модус поненс также может быть применено к выражениям, содержащим переменные. Рассмотрите в качестве примера обычный силлогизм "все люди смертны, и Сократ — человек, поэтому Сократ — смертен". Высказывание "Все люди смертны" может быть представлено в исчислении предикатов (по-русски и по-английски) так.
Поскольку X в выражении стоит под знаком квантора всеобщности, его можно заменить любым значением из области определения X, и при этом утверждение будет сохранять истинное значение согласно правилу универсального инстанцирования. Заменив в выражении X на сократ, получим следующее утверждение.
Применив правило модус поненс, приходим к выводу mortal(socrates). Он может быть добавлено к набору выражений, которые логически следуют из первоначальных утверждений. Можно использовать так называемый алгоритм унификации для определения автоматическим решающим устройством правомочности замены X на socrates и возможности применения правила модус поненс. Унификация обсуждается в подразделе 2.3.2.
В главе 12 обсуждается более строгое правило вывода, называемое правилом резолюции (resolution), которое является основой многих интеллектуальных автоматических систем.
