й шаг вывода в этом случае связан всегда с первоначально поставленной целью. Существенный недостаток метода резолюции заключается в формировании на каждом шаге вывода множества резольвент - новых дизъюнктов, большинство из которых оказывается лишними. В связи с этим разработаны различные модификации принципа резолюции, использующие более эффективные стратегии поиска и различного рода ограничения на вид исходных дизъюнктов. В этом смысле наиболее удачной и популярной является система ПРОЛОГ, которая использует специальные виды дизъюнктов, называемых дизъюнктами Хорна.
Процесс доказательства методом резолюции (от обратного) состоит из следующих этапов:
1. Предложения или аксиомы приводятся к дизъюнктивной нормальной форме.
2. К набору аксиом добавляется отрицание доказываемого утверждения в дизъюнктивной форме.
3. Выполняется совместное разрешение этих дизъюнктов, в результате чего получаются новые основанные на них дизъюнктивные выражения (резольвенты).
4. Генерируется пустое выражение, означающее противоречие.
5. Подстановки, использованные для получения пустого выражения, свидетельствуют о том, что отрицание отрицания истинно.
Рассмотрим примеры применения методов поиска решений на основе исчисления предикатов. Пример "интересная жизнь" заимствован из 1. 1 . Итак, заданы утверждения 1-4 в левом столбце таблица 3. 2 Требуется ответить на вопрос: "Существует ли человек, живущий интересной жизнью?" В виде предикатов эти утверждения записаны во втором столбце таблицы. Предполагается, что . В третьем столбце таблицы записаны дизъюнкты.
Таблица 3. 2. Интересная жизнь
Утверждения и заключение
Предикаты
Предложения(дизъюнкты)
1. Все небедные и умные люди счастливы
2. Человек, ч
Страницы: << < 9 | 10 | 11 | 12 | 13 > >>