logic - 不动点和证明理论

Question

对于任何给定的逻辑程序，它的证明理论使用 SLD（选择性线性定）分辨率来找到查询的可满足性。对于相同的逻辑程序，我们可以应用不动点定理来找到模型。

我的问题是，

我们应该考虑将逻辑程序的不动点作为证明理论或模型理论，还是两者都不是？

Answer 1

我的猜测是模型理论，因为逻辑程序的定点语义就是它的模型。但是，我们知道这|=与|-逻辑程序相吻合，因此基于证明（=分辨率）的语义与基于不动点（模型）的语义相吻合。

前面的讨论只对纯逻辑程序有效，即没有否定、bultins、算术......