語句の真相とあやまち

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

ResolutionPrinciple

こんな証明はできないのか

clauseの集合を {P(a), Q(a), Q(b)} としたとき any x. P(x) → Q(x) は証明できるのか? できないみたい。 Herbrand Universeで成り立っても、必ずしも成り立たないようなかんじ。 もしも、 {P(a), P(f(x))} で P(f(x)) の証明は当然できる。

そしてResolution

Juliaで論理式を表す方法について、ずっと試行錯誤している。 いまは、parse("[x,y].[+P(x,f(x)),-Q(x,y)]") のようにparse()を使うことにして、Exprベースで式を扱っている。 内部で[x,y] と :([+(P(x,f(x)),-(Q(x,y))] に分けているのだけれど、これも[:(+…

それから Resolutionにいたるまで

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