【发布时间】：2015-05-01 18:07:52
【问题描述】：
对于任何给定的逻辑程序，它的证明理论使用 SLD（选择性线性定）解析来找到查询的可满足性。对于同样的逻辑程序，我们可以应用不动点定理来寻找模型。
我的问题是，
我们应该考虑寻找逻辑程序的不动点作为证明论还是模型论，还是两者都不是？
【问题讨论】：
-
这个问题是针对这个区域还是其他地方？对于这样的理论问题，您可能会在其他溢出板上得到更好的答案。
-
@MichaelDorgan cs.stackexchange.com?
-
这不是计算机科学的完全理论部分。
-
不知道。这已经在这里待了将近一个小时，没有真正的帮助。我几乎无法理解这个问题，但是当涉及到这样的事情时，我并不是受过最多教育的人。只是想让你更多地关注你的问题。
-
模型论和证明论是赋予给定逻辑程序意义的不同方式。我碰巧解决了使用定点语义。我不知道定点语义在哪里适合。doc.ic.ac.uk/~mjs/teaching/KnowledgeRep491/…
标签： logic proof logic-programming first-order-logic