MINLOG の変更点

• 追加された行はこの色です。
• 削除された行はこの色です。
• MINLOG へ行く。

*MINLOG [#k1c911fb]

MINLOG is based on first order natural deduction calculus. It is intended to reason about computable functionals, using minimal rather than classical or intuitionistic logic. The system is supported by automatic proof search and normalization by evaluation as an efficient term rewriting device.

MINLOG は Scheme 上で動く，自然演繹による一階述語最小論理の対話的定理証明器です．

*インストール例 [#d8fc51cf]

 sudo apt-get -y install guile-2.0
 export CAS=/usr/local/CAS
 sudo mkdir $CAS
 sudo chmod 777 $CAS
 cd $CAS
 wget http://www.mathematik.uni-muenchen.de/~logik/minlog/cronfiles/minlog-latest.tar.gz
 tar zxvf ./minlog-latest.tar.gz
 rm ./minlog-latest.tar.gz
 cd ./minlog
 make
 sudo ln -s /usr/local/CAS/minlog/minlog /usr/local/bin/minlog

*使用例 [#qc6133f8]

起動

 cd /usr/local/CAS/minlog
 rlwrap guile -l ./init.scm

（emacs で用いる場合は

 minlog

）

0項述語（命題）変数を追加

 (add-pvar-name "A" "B" "C" (make-arity))

（emacs で用いる場合はカーソルを行末において，C-x C-e）

ゴールを設定

 (set-goal (pf "(A -> B -> C) -> (A -> B) -> A -> C"))

証明を検索（ search は最小論理の範囲で述語論理まで扱えるコマンド）

 (search)

証明を表示

 (dnp)

古典論理の例，ゴールを設定

 (set-goal (pf "((A -> B) -> A) -> A"))

仮定にチャージ

 (assume 1)

二重否定消去の明示的利用

 (use "Stab")
 (assume 2)

仮定を利用

 (use 2)
 (use 1)
 (assume 3)

principle of explosion (ex falso quodlibet) の明示的利用

 (use "Efq")
 (use-with 2 3)
 (dnp)

証明の検索（ prop は命題論理の範囲で古典論理まで扱えるコマンド）

 (set-goal (pf "((A -> B) -> A) -> A"))
 (prop)
 (dnp)

述語論理の例

 (add-pvar-name "P" (make-arity (py "alpha")))
 (add-var-name "x" (py "alpha"))
 (set-goal (pf "all x (P x) -> ex x (P x)"))
 (search)
 (dnp)

終了

 (exit)

*リンク [#gf7434f0]
- http://www.mathematik.uni-muenchen.de/~logik/minlog/index.php