近況　mguをプログラムとみなしたい

clauseの集合Σが与えられた時、Σの中に存在する可能なすへてのmguの集合M = {<L1:L2>| ∀Li ∈ ∀c ∈Σ}は有限であり、Σからのどの証明もその各stepのmguはこのMのどれかのインスタンス(代入{x←t1} が {x←t2}のインスタンスである({x←t1} ⊑ {x←t2})とはt1⊑t2であること)になっている。

resolutionでは、pairとするclauseごとに共通変数がないことが必要なので、もしも同じ変数が出現していたら話がややこしなくなるだろう。それは解決できているので、今後は、共通変数が一切ないとして話を進める。

ということは、Σからの証明は、Mのmguを組み合わせればできてしまうということではないのだろうか。
実際にその「組み合わせ」を作るところが容易ではないので、この方法が証明を簡単にするように見えるかもしれないけど、実際の述語論理の証明をすることはやはり難しいということになる。

プログラムと証明の違いは、このMに述語記号が存在しないところにあると思う。Σの証明は述語記号とその引数のタプルによって値のタブルに対する制約条件が表されているが、Mはその制約がない。ただし、上に書いたように変数が混在しないようにできていれば、述語のかわりに変数名の同一性でMをもとに証明を解釈することができるだろう。と想像している。

そういうわけで、最近考えているのは、このMをひとつのプログラミング言語とみなせないかということなのだが、Mの実行が証明をなぞっているだけなので、ときどき訳がわからなくなる。いや勿論、証明をなぞっているから、Mの実行が証明と結びついているわけだけれど。

mguを計算言語とみなすということは、論理式が表している計算過程の集合の表現として、述語を含まないmguの集合を使うということであり、それはprologのような言語を述語のない形式に変換するということだから、Prolog関連の文献にそういう方法について書かれたものがあるかもしれない。

調べきれなかった。