プログラミング言語の基礎概念 p.4 導出システム Nat

gistfile1.txt

; try the following code at http://rise4fun.com/z3/tutorial
; data type Nat
(declare-datatypes () ((Nat zero (succ (pred Nat)))))
; plus as a rule
(declare-fun plus (Nat Nat Nat) Bool)
; rule P-Zero
(assert (forall ((n Nat)) (plus zero n n)))
; rule P-succ
(assert (forall ((m Nat) (n Nat) (r Nat))
  (=> (plus m n r) (plus (succ m) n (succ r)))))
; step 0
(assert (plus zero zero zero))
; (check-sat)
; step 1
(assert (plus zero (succ zero) (succ zero)))
; step 2
(assert (plus (succ zero) (succ zero) (succ (succ zero))))
(check-sat)

gistfile2.txt

すみません、この定義では不十分でした

https://twitter.com/ikegami__/status/624498576865890304
https://twitter.com/ikegami__/status/624507334304239617
https://twitter.com/ikegami__/status/624508974977564672
http://rise4fun.com/z3/tutorial

などなど…

だれか Z3 でできるよということであれば
@ikegami__
に教えてくれると嬉しいです