moratori / flexpr Goto Github PK

等号公理x=xを入れて導出によってx≠xが矛盾することを導かなければいけないのに、今の実装だと、節集合の単節にx≠xが存在するかを確認してるだけなのでa=a&b=bのような式が証明できなくなっている

置換σの定義域がそもそも対象のリテラルに含まれていない時に、LσはLそのものを表すが、paramod-unifyのremoveでLが削除されてしまうので返す節がなくなりタイプエラーとなる.

等式をE、リテラルLとするときにLに出現するEの左辺と等しい項を全てEの右辺に書き換えてしまうのがよろしくない。正確にいうと、Lに出現するEの左辺と等しい各項について、置き換えるor置き換えないの全ての組み合わせをparamodulantとすべき。(但しもの凄い数の節が生成される)

存在量化子のついた特定の式で、項を求めると項がおかしいことがある。
factファイルを読み込んで Ex.!(s(s(s(s(ZERO)))),x) をやると
x = 21になる. 4! = 24なのに