Нет конечно провальных производных. Только неудачные дифференцирования и конечно неудачные дифференцирующие деревья. Неудачные деривации - это деривация, которая заканчивается неудачей. Например:
p :- q.
p :- p.
q :- fail.
Деривация, состоящая из первого правила p, а затем единственного правила q, является неудачной деривацией. Производные могут не только потерпеть неудачу, потому что неопределенный предикат, такой как fail, но также и потому, что некоторое объединение головы не полностью завершается успешно.
Теперь, что такое дерево с конечным провалом? Хорошо, если вы посмотрите на все деривации, вы получите дерево. В дереве с конечными ошибками деривация является конечной, и каждая деривация является неудачной. Конечно, деривационные деревья имеют следующее хорошее свойство:
- The interpreter terminates.
- The interpreter does not produce any answer substitution.
В практических системах Prolog это означает, что после постановки вопроса вы через некоторое время получите «Нет» (в некоторых системах Prolog отображается false). Интересно, что вышеприведенная программа не завершится для запроса p. Это экземпляр бесконечного деривационного дерева, в котором каждое деривация не удалась. Выводы:
p - q - fail
p - p - q - fail
p - p - p - q - fail
Etc..
Понятие конечно-неудачных деревьев деривации определено для определенных программ Пролога. Теперь можно расширить понятие программы Пролог на общие программы Пролог. В общей программе Prolog тело может содержать отрицательные литералы. И идея состоит в том, что интерпретатор регрессирует к проверке конечных неудачных деревьев деривации для этих литералов.
Одним из важных вопросов является то, как деревья с конечными ошибками связаны с математическими производными. При какой математической семантике цель может потерпеть неудачу? И как мы можем построить интерпретатор, который реализует эту семантику? Особый класс семантики основан на методе опровержения. Здесь мы объясняем вывод как установление противоречия:
P, ~G |= f => P |- G
Это более или менее подразумевает устранение двойного отрицания и, следовательно, классическую логику. Но и другие логики могут быть полезными. Для начала вы можете посмотреть следующую книгу:
Логика для приложений
Анил Нероде, Ричард А. Шор
Второй. Издание 1997 года, Springer
Bye