MINLOG

MINLOG †

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 上で動く，自然演繹による一階述語最小論理の対話的定理証明器です．

インストール例 †

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

使用例 †

起動

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)

リンク †

• http://www.mathematik.uni-muenchen.de/~logik/minlog/index.php

最新の20件