世界で一番ピュアな論理型プログラミング言語Hilbert(ヒルベルト)をRubyで作った. ref: http://qiita.com/gogotanaka/items/97ae187156541c8eaa9d

file0.coffee

A       # 命題Aが真である事の宣言
A -> B  # 命題A->Bが真である事の宣言
B?      # Aが真かつA-BならばBは真
#=> TRUE

file1.coffee

# 三段ロンポー
P -> Q
Q -> R
P -> R ?
=> TRUE

P | Q # PまたはQ
~P    # Pではない
Q?    # ではQである
=> TRUE

A?
=> UNDEFINED
~A
A?
=>FALSE

A -> B    # AならばBである
B -> A ?  # BならばAとは限らない
=> UNDEFINED
B -> A    # BならばAである
A <-> B ? # AとBは同値である

# 標準の公理系をインポートすれば実数解析なども扱える
postulate zfc_analysis

d/dx x^2
=> 2x

d/dx e^x
=> e^x

S(sin(x)dx)[0..pi]
=> 2

lim[x->oo] 1/x
=> 0

∑[i=1, 10] i
=> 55

file10.txt

f(x, y) = x + y

f(2, 2)
=> 4

g(x) = x ** 2

g(2)
=> 4

file11.txt

$  gem install hilbert

file12.txt

$  echo "gem 'hilbert'" >> ~/.Gemfile; bundle install

file13.txt

$  hilbert -i
Enjoy! -> 

file14.txt

$  hilbert -i -zfc
Enjoy! -> 

file15.txt

$ hilbert -r foo.hr

file16.txt

$ hilbert -rb foo.hr

file17.txt

$ hilbert -py foo.hr

file2.txt

IsHuman(gogotanaka)           # gogotanakaは人間である
A[x] IsHuman(x) -> WillDie(x) # 全ての人間は死ぬ
WillDie(gogotanaka)?          # gogotanakaは死ぬのか？
#=>true

file3.txt

gogotanaka <- HUMAN    # gogotanakaは人間である.
A[h<-HUMAN] WillDie(h) # 全ての人間は死ぬ
WillDie(gogotanaka)?   # gogotanakaは死ぬのか？
#=>true

file4.txt

Axiom tanaka
  A
  A->B
end

postulate tanaka #公理系の仮定(事実モジュールのインポート)

file5.coffee

A     # Aは真
A->B  # AならばBも真
B?    # Bも真
#=> true

A->B
B->C
(A->C)?
#=> true

file6.coffee

A  # Aは真である
~A # Aは偽でもある

paradox?
=> TRUE

file7.txt

d/dx(cos(x))
=> ( - sin( x ) )

d/dx(log(x))
=> ( 1 / x )

d/dy(y ** 2)                        
=> ( 2 * y )

d/dz(e ** z)                        
=> ( e ** z )

file8.txt

S(log(x)dx)[0..1]
=> - oo

S( sin(x)dx )[0..pi]
=> 2.0

S( cos(x)dx )[0..pi]                       
=> 0.0

file9.txt

(1 2 3; 4 5 6)
=> (1 2 3; 4 5 6)

(1 2 3; 4 5 6) + (1 2 3; 4 5 6)
=> (2 4 6; 8 10 12)

(1 2 3; 4 5 6) * (1 2 3)
=> (14 32)