Интеллектуальные робототехнические системы


Методы поиска решений на основе исчисления предикатов - часть 3


заменяются на

импликацию.

Вернемся к принципу резолюции. Главная идея этого правила вывода заключается в проверке того, содержит ли множество дизъюнктов R пустой (ложный) дизъюнкт. Обычно резолюция применяется с прямым или обратным методом рассуждения. Прямой метод из посылок A, A

B выводит заключение B (правило modus ponens). Основной недостаток прямого метода состоит в его не направленности: повторное применение метода приводит к резкому росту промежуточных заключений, не связанных с целевым заключением. Обратный вывод является направленным: из желаемого заключения B и тех же посылок он выводит новое подцелевое заключение A. Каждый шаг вывода в этом случае связан всегда с первоначально поставленной целью. Существенный недостаток метода резолюции заключается в формировании на каждом шаге вывода множества резольвент - новых дизъюнктов, большинство из которых оказывается лишними. В связи с этим разработаны различные модификации принципа резолюции, использующие более эффективные стратегии поиска и различного рода ограничения на вид исходных дизъюнктов. В этом смысле наиболее удачной и популярной является система ПРОЛОГ, которая использует специальные виды дизъюнктов, называемых дизъюнктами Хорна.

Процесс доказательства методом резолюции (от обратного) состоит из следующих этапов:

  1. Предложения или аксиомы приводятся к дизъюнктивной нормальной форме.
  2. К набору аксиом добавляется отрицание доказываемого утверждения в дизъюнктивной форме.
  3. Выполняется совместное разрешение этих дизъюнктов, в результате чего получаются новые основанные на них дизъюнктивные выражения (резольвенты).
  4. Генерируется пустое выражение, означающее противоречие.
  5. Подстановки, использованные для получения пустого выражения, свидетельствуют о том, что отрицание отрицания истинно.

Рассмотрим примеры применения методов поиска решений на основе исчисления предикатов. Пример "интересная жизнь" заимствован из [2]. Итак, заданы утверждения 1-4 в левом столбце таблица 3.2

Требуется ответить на вопрос: "Существует ли человек, живущий интересной жизнью?" В виде предикатов эти утверждения записаны во втором столбце таблицы.


Начало  Назад  Вперед