logic - 不動点と証明理論

Question

任意の論理プログラムについて、その証明理論は SLD (Selective Linear Definite) 解決を使用してクエリの充足可能性を見つけます。同じ論理プログラムに対して、不動点定理を適用してモデルを見つけることができます。

私の質問は、

論理プログラムの不動点を証明理論やモデル理論として考えるべきか、それともどちらでもないのか?

Answer 1

ロジック プログラムの固定点セマンティクスはそのモデルであるため、私の推測ではモデル理論になります。|=しかし、論理プログラムの場合は一致することがわかっている|-ので、証明(=解決)に基づく意味論は、不動点(モデル)に基づく意味論と一致します。

前述の説明は、純粋な論理プログラム、つまり、否定、ブルティン、算術演算などのプログラムに対してのみ有効です...