При прямом ходе доказательства некоторой цели отсечение выступает как истинное условие в теле правила и не оказывает никакого воздействия на процесс выполнения. Его назначение реализуется только при инициировании процесса возврата вследствие ложности одного из предикатов, расположенных после (справа или ниже) отсечения в теле правила. В этом случае, т.е. при прохождении отсечения в обратном направлении (справа налево), оно как бы объявляет, что цель, вызвавшая выполнение отсечения (родительская цель), не имеет других вариантов согласования, а потому процесс возврата осуществляется к предшествующей (расположенной левее от родительской) цели.
Другими словами, действие отсечения при возврате сводится к следующим моментам:
• отсечение выбрасывает из рассмотрения все утверждения, расположенные после предложения, в котором находится отсечение;
• отсечение отбрасывает все альтернативные решения конъюнкции целей, расположенных в утверждении левее отсечения, т.е. конъюнкция целей, стоящих перед отсечением, приводит не более чем к одному решению;
• отсечение не влияет на цели, расположенные правее его. В случае возврата они могут порождать более одного решения.
Таким образом, отсечение при возврате сокращает пространство поиска вариантов доказательства.
Опубликовал Kest
November 05 2009 14:43:45 ·
0 Комментариев ·
5504 Прочтений ·
• Не нашли ответ на свой вопрос? Тогда задайте вопрос в комментариях или на форуме! •
Комментарии
Нет комментариев.
Добавить комментарий
Рейтинги
Рейтинг доступен только для пользователей.
Пожалуйста, залогиньтесь или зарегистрируйтесь для голосования.
Нет данных для оценки.
Гость
Вы не зарегистрированны? Нажмите здесь для регистрации.
Главная
Каталог файлов
