λx,z,E.y F(x,y),F(y,z)→F(x,z)

clause形に変換するとき、違うclauseの変数は独立になる。 λx,z,E.y F(x,y),F(y,z)→F(x,z) は、全順序のようにも見えるが本当は、友達の友達は友達の関係。 ここでは、yが存在すればF(x,z)であるということで、存在が重要。 存在を全称にしてしまってこれをc…

Factのadjustについて

Factの述語記号P、定数記号cとし、FactにP(c)が含まれていないとき Pが2つに一つだったら、-P(c)を加えてもいいはず。つまり、G(x)が'xは少女'という意味なら、FactにG(c)が含まれていなければ'-G(c)'にしても、だいたい正しい 一方で、友達を表す'F(x,y)'に…

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

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

Project EulerをJuliaでやる

Projct EulerをJuliaで解いてみる。 以前は、RubyかRかで20個くらい解いたあと、問題が面倒臭いのばかりで放棄していたのだけれど、途中で言語を変えるのもおもしろくないから、改めてJuliaで解くためにアカウントを新調してみた。 解法をブログに書くのは問…

The Little Prover

これは、LISPやSchemeに対する、The Little LisperやThe Little Schemerのような関係にある Coqに対するThe Little Proferらしい。 まだ最初の方しか読めていない。ややこしい。 focusをあてている部分にルールを適用するその仕方を繰り返し説明しているのだ…

Deviant Moon Tarot Companion Book by Patrick Valenza

数日前にAmazon.co.jpから届けられたこの本は、思っていたよりも巨大。 しかし、大きな絵がとてもいい。 元のタロットは、従来のタロットとはまったく違う絵だと思う。 不思議な絵で、見ているといろんなストーリーが浮かんでくる。 時間がいくらでもすぎて…