Archive
自動証明処理系の coq を使って簡単な3段論法を証明してみる。
まず coq を起動する。
% coqtop Coq <
命題 A B C について考えてみるよ。
Coq < Variables A B C : Prop. A is assumed B is assumed C is assumed
「A ならば B 」といのは命題だよね?
Coq <…
