語句の真相とあやまち

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

そしてResolution

Juliaで論理式を表す方法について、ずっと試行錯誤している。

いまは、parse("[x,y].[+P(x,f(x)),-Q(x,y)]") のようにparse()を使うことにして、Exprベースで式を扱っている。

内部で[x,y] と :([+(P(x,f(x)),-(Q(x,y))] に分けているのだけれど、これも[:(+(P(x,f(x)))), :(-(Q(x,y))]にしたほうがいいかもしれない。

 

Resolutionについては、だいぶ忘れてしまったので、思い出すためにいろいろ調べているけれど、今のAIブームの中では自動証明はほとんど話題になっていないように見える。

 ニューラルネットと自動証明はAIの両輪のような気がするけれど、そうでもないのかもしれない。そもそもAIという言葉も意味不明ではあるけど。

 

話題がそれたので戻すと、unificationはできていて、単体のResolutionもできているはず。

あとはclause集合からcontradictionを導出するtactics/strategyをどうするか・・・

 

まず、命題論理でgoalからの証明の枠組みを作り、一階でその証明にmguが存在するかどうかでステップの刈り込みを行う。

このとき、繰り返される証明ステップパターンが無限の証明になるのをどうするか。

 

これは先の場合と同じく、

  • 世界の事実(Fact)をground unit clauseの集合で表し
  • それに対する仮説(理論, Theory)を変数を含むclauseの集合で表す
  • queryはいまのところunit clauseを想定

というようなもの。

仮説は、すべてのFactについて成立するものを考えているので、少なくとも

Fact + Theory は無矛盾にしたい。これは、Theoryの各clauseをFactに加えたとき矛盾がでないことで分かるが、たぶん有限時間に検証できるだろう。

複数のTheoryの間の矛盾は有限時間では分からないかもしれない。たぶん分からない。