一階述語論理

Prolog に一コマ取ってるので、定義と説明があるのだが

　　Agda でやるよね?

で data で構文定義していく方式で。割とすぐに書けたんですが、やっぱり構文ださいよねで、parser 書いたら思いっきり複雑に。

特に証明しているわけでもないのでHaskellでいいんだど。paeser は諦めて、

　　ex1 : Statement
　　ex1 = All X => All Y => (( Exist Z =>
　　　 ( ( predx father ( var X , var Z ) ∧　predx father (var Y , var Z ) ))) ⇒ predx brother ( var X , var Y) )

これくらいで妥協か。で、Star Wars のねたばれ例題をやるわけですが。

　　brother ( const leia , const leia) = true

あぁ、この定義ではそうなるか。ま、いいよね。

　　data Var : Set where
　　　　　X : Var
　　　　　Y : Var
　　　　　Z : Var

　　data Func : Set where

　　data Pred : Set where
　　　　　father : Pred
　　　　　brother : Pred

　　data Expr　: Set　where
　　　 var　 : Var　 → Expr
　　　 func　: Func　→ Expr → Expr
　　　 const : Const → Expr
　　　 _,_　 : Expr　→ Expr → Expr

　　data Statement : Set where
　　　 pred　　　 : Pred　　　→ Statement
　　　 predx　　　: Pred　　　→ Expr　　　→ Statement
　　　 _∧_　　　　: Statement → Statement → Statement
　　　 _∨_　　　　: Statement → Statement → Statement
　　　 ¬_　　　　 : Statement → Statement
　　　 All_=>_　　: Var　　　 → Statement → Statement
　　　 Exist_=>_　: Var　　　 → Statement → Statement


　　_⇒_ : Statement → Statement → Statement
　　x ⇒ y = ( ¬ x ) ∨ y

Interpretationと節形式への変換までできたのでいろいろインチキはあるが問題ない感じ。Eqaulity 入れるとぐっと難易度が上がるらしい。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/FirstOrder