Теория фиксированной точки и доказательства

Question

Для любой заданной логической программы в ее теоретической теории используется SLD (выборочное линейное определение), чтобы найти удовлетворительность запроса. Для той же логической программы мы можем применить теорему с фиксированной точкой, чтобы найти модели.

Мой вопрос,

мы должны рассматривать найти неподвижную точку логических программ, как доказательство теории или теории моделей или это ни?

Answer 1

Мое предположение было бы модель теории, поскольку семантика фиксированной точки логической программы является ее моделью. Однако мы знаем, что |= совпадает с |- для логических программ, поэтому семантика, основанная на доказательстве (= разрешение), совпадает с семантикой на основе неподвижных точек (моделей).

Предшествующее обсуждение справедливо только для чисто логических программ, то есть, нет отрицаний, bultins, арифметики ...