語句の真相とあやまち

なにもないことにまつわるあれこれとか関係のないこととか

それから Resolutionにいたるまで

JuliaでResolutionをしたいと思っていたのだけれど、式の表現でSymbolを使うといちいち:なんとかと書かなくてはならないことや、Lispだとlistにするところをベクトルにした場合の表現方法などで悩んで、手がつかなかったのが、去年のどこかでそのあたりがわかったので、いろいろとプログラムを作っている。

最初に作ったのは、非常に単純なものというか制限をつけたもので、それがだいたいできた段階で、真面目に1階述語のResolutionを作った。

 

今は、Unit resolutionあるいはLinear Resolutionで証明(あるいは反証)を作るあたりを考えている。

 

最初に作ったものでは

1. 世界の事実を記述したUnit Clauseの集合に対して、Queryとしての論理式が与えられると、その変数に対する代入を解=モデルを求めるというもの。

DBのQueryみたいなものだ(歴史的には逆か)

 

事実は変数を含まないので、resolutionも一方向の代入だけを考えればよく、事実の全Factを列、QueryのClauseの各Literalを行とし、成分にmguをとるような行列を考える。

その行列を元に、代入の積を使ってQuery全体で成立するモデルを絞り込むというようなもの。

いくつかサンプルをやってみると、あまり深い答えはでなかった。

これはこれで面白いのだけれど、まともな一階述語論理のシステムにしてみようと思うようになったという次第。