Семантика исчисления предикатов обеспечивает основу для формализации логического вывода. Возможность логически выводить новые правильные выражения из набора истинных утверждений очень важна. Логически выведенные утверждения корректны, и они совместимы со всеми предыдущими интерпретациями первоначального набора выражений. Обсудим вышесказанное неформально и затем введем необходимую формализацию.
В исчислении высказываний основным объектом является переменное высказывание (предикат), истинность или ложность которого зависит от значений входящих в него переменных. Так, истинность предиката "x был физиком" зависит от значения переменной x. Если x - П. Капица, то предикат истинен, если x - М. Лермонтов, то он ложен. На языке исчисления предикатов утверждение x(P(x) Q(x)) читается так: "для любого x если P(x), то имеет место и Q(x)". Иногда его записывают и так: x (P(x) Q(x)). Выделенное подмножество тождественно истинных формул (или правильно построенных формул - ППФ), истинность которых не зависит от истинности входящих в них высказываний, называется аксиомами.
В исчислении предикатов имеется множество правил вывода. В качестве примера приведем классическое правило отделения, или modus ponens :
(A, A B) / Bкоторое читается так "если истинна формула A и истинно, что из A следует B, то истинна и формула B". Формулы, находящиеся над чертой, называются посылками вывода, а под чертой - заключением. Это правило вывода формализует основной закон дедуктивных систем: из истинных посылок всегда следуют истинные заключения. Аксиомы и правила вывода исчисления предикатов первого порядка задают основу формальной дедуктивной системы, в которой происходит формализация схемы рассуждений в логическом программировании. Можно упомянуть и другие правила вывода.
Modus tollendo tollens : Если из A следует B и B ложно, то и A ложно.
Modus ponendo tollens : Если A и B не могут одновременно быть истинными и A истинно, то B ложно.
Modus tollendo ponens : Если либо A, либо B является истинным и A не истинно, то B истинно.
Решаемая задача представляется в виде утверждений (аксиом) f1, F2... Fn исчисления предикатов первого порядка. Цель задачи B также записывается в виде утверждения, справедливость которого следует установить или опровергнуть на основании аксиом и правил вывода формальной системы. Тогда решение задачи (достижение цели задачи) сводится к выяснению логического следования (выводимости) целевой формулы B из заданного множества формул (аксиом) f1, F2... Fn. Такое выяснение равносильно доказательству общезначимости (тождественно-истинности) формулы
f1& F2&... & Fn Bили невыполнимости (тождественно-ложности) формулы
f1& F2&... & Fn& ¬BИз практических соображений удобнее использовать доказательство от противного, то есть доказывать невыполнимость формулы. На доказательстве от противного основано и ведущее правило вывода, используемое в логическом программировании, - принцип резолюции. Робинсон открыл более сильное правило вывода, чем modus ponens, которое он назвал принципом резолюции (или правилом резолюции ). При использовании принципа резолюции формулы исчисления предикатов с помощью несложных преобразований приводятся к так называемой дизъюнктивной форме, то есть представляются в виде набора дизъюнктов. При этом под дизъюнктом понимается дизъюнкция литералов, каждый из которых является либо предикатом, либо отрицанием предиката.
Приведем пример дизъюнкта:
x (P(x, c1) Q(x, c2)).Пусть P - предикат уважать, c1 - Ключевский, Q - предикат знать,c2 - история. Теперь данный дизъюнкт отражает факт "каждый, кто знает историю, уважает Ключевского".
Приведем еще один пример дизъюнкта:
x (P(x, c1)& P(x, c2)).Пусть P - предикат знать, c1 - физика, c2 - история. Данный дизъюнкт отражает запрос "кто знает физику и историю одновременно".
Таким образом, условия решаемых задач (факты) и целевые утверждения задач (запросы) можно выразить в дизъюнктивной форме логики предикатов первого порядка. В дизъюнктах кванторы всеобщности , , обычно опускаются, а связки , ¬, заменяются на импликацию.
Вернемся к принципу резолюции. Главная идея этого правила вывода заключается в проверке того, содержит ли множество дизъюнктов R пустой (ложный) дизъюнкт. Обычно резолюция применяется с прямым или обратным методом рассуждения. Прямой метод из посылок A, A B выводит заключение B (правило modus ponens). Основной недостаток прямого метода состоит в его не направленности: повторное применение метода приводит к резкому росту промежуточных заключений, не связанных с целевым заключением. Обратный вывод является направленным: из желаемого заключения B и тех же посылок он выводит новое подцелевое заключение A. Каждый шаг вывода в этом случае связан всегда с первоначально поставленной целью. Существенный недостаток метода резолюции заключается в формировании на каждом шаге вывода множества резольвент - новых дизъюнктов, большинство из которых оказывается лишними. В связи с этим разработаны различные модификации принципа резолюции, использующие более эффективные стратегии поиска и различного рода ограничения на вид исходных дизъюнктов. В этом смысле наиболее удачной и популярной является система ПРОЛОГ, которая использует специальные виды дизъюнктов, называемых дизъюнктами Хорна.
Процесс доказательства методом резолюции (от обратного) состоит из следующих этапов:
Рассмотрим примеры применения методов поиска решений на основе исчисления предикатов. Пример "интересная жизнь" заимствован из [2]. Итак, заданы утверждения 1-4 в левом столбце таблица 3.2 Требуется ответить на вопрос: "Существует ли человек, живущий интересной жизнью?" В виде предикатов эти утверждения записаны во втором столбце таблицы. Предполагается, что X(smart(X)=¬stupid(X)) и Y(wealthy(Y)=¬poor(Y)). В третьем столбце таблицы записаны дизъюнкты.
Таблица 3.2. Интересная жизнь | ||
Утверждения и заключение | Предикаты | Предложения(дизъюнкты) |
1. Все небедные и умные люди счастливы | X(¬poor(X) smart(X) happy(X)) | poor(X) ¬smart(X) & happy(X) |
2. Человек, читающий книги, - неглуп | Y (read(Y) smart(Y)) | ¬read(Y) & smart(Y) |
3. Джон умеет читать и является состоятельным человеком | read(John) ¬poor(John) | 3a read(John)3b ¬poor(John) |
4. Счастливые люди живут интересной жизнью | Z (happy(Z)exciting(Z)) | ¬happy(Z)&exciting(Z) |
5. Заключение: Существует ли человек, живущий интересной жизнью? | W(exciting(W)) | exciting(W) |
6. Отрицание заключения | ¬W(exciting(W)) | ¬exciting(W) |
Отрицание заключения имеет вид (строка 6): ¬W(exciting(W))
Одно из возможных доказательств (их более одного) дает следующую последовательность резольвент:
Символ NIL означает, что база данных выражений содержит противоречие и поэтому наше предположение, что не существует человек, живущий интересной жизнью, неверно.
В методе резолюции порядок комбинации дизъюнктивных выражений не устанавливался. Значит, для больших задач будет наблюдаться экспоненциальный рост числа возможных комбинаций. Поэтому в процедурах резолюции большое значение имеют также эвристики поиска и различные стратегии. Одна из самых простых и понятных стратегий - стратегия предпочтения единичного выражения, которая гарантирует, что резольвента будет меньше, чем наибольшее родительское выражение. Ведь в итоге мы должны получить выражение, не содержащее литералов вообще.
Среди других стратегий (поиск в ширину (breadth-first), стратегия "множества поддержки", стратегия линейной входной формы) стратегия "множества поддержки" показывает отличные результаты при поиске в больших пространствах дизъюнктивных выражений [2]. Суть стратегии такова. Для некоторого набора исходных дизъюнктивных выражений S можно указать подмножество T, называемое множеством поддержки. Для реализации этой стратегии необходимо, чтобы одна из резольвент в каждом опровержении имела предка из множества поддержки. Можно доказать, что если S - невыполнимый набор дизъюнктов, а S-T - выполнимый, то стратегия множества поддержки является полной в смысле опровержения. С другими стратегиями для поиска методом резолюции в больших пространствах дизъюнктивных выражений читатель может познакомиться в специальной литературе [2], [45], [46].
Исследования, связанные с доказательством теорем и разработкой алгоритмов опровержения резолюции, привели к развитию языка логического программирования PROLOG (Programming in Logic). PROLOG основан на теории предикатов первого порядка. Логическая программа - это набор спецификаций в рамках формальной логики. Несмотря на то, что в настоящее время удельный вес языков LISP и PROLOG снизился и при решении задач ИИ все больше используются C, C++ и Java, однако многие задачи и разработка новых методов решения задач ИИ продолжают опираться на языки LISP и PROLOG. Рассмотрим одну из таких задач - задачу планирования последовательности действий и ее решение на основе теории предикатов.