MINLOG
の編集
http://www.mathlibre.org/wiki/?MINLOG
[
トップ
] [
編集
|
差分
|
バックアップ
|
添付
|
リロード
] [
新規
|
一覧
|
検索
|
最終更新
|
ヘルプ
]
-- 雛形とするページ --
(no template pages)
*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
タイムスタンプを変更しない
*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
テキスト整形のルールを表示する