对于任何给定的逻辑程序，它的证明理论使用SLD（选择性线性定定）分辨率来找到查询的满足性。对于相同的逻辑程序，我们可以应用不动点定理来查找模型。
我的问题是，
我们应该考虑找到逻辑程序的不动点作为证明理论或模型理论还是两者都不是？
我的猜测是模型论，因为逻辑程序的定点语义是它的模型。但是，我们知道|=与逻辑程序的|-一致，因此基于证明（=分辨率）的语义与基于不动点（模型）的语义一致。
前面的讨论只对纯逻辑程序有效，即无否定、不否定、算术......