読者です 読者をやめる 読者になる 読者になる

kivantium活動日記

プログラムを使っていろいろやります

LaTeXによる証明図の記述

証明図は「bussproof.sty」にお任せを参考にいくつか証明図を書いてみました。ひな形はこんな感じです。

\documentclass{jsarticle}
\pagestyle{empty}
\usepackage{bussproofs}

\begin{document}

\begin{prooftree}
%ここに証明図を書く
\end{prooftree}
\end{document}

以下は省略してprooftree環境の中だけ書きます。
まずは簡単なものから

\AxiomC{$(\Phi \land \Psi)$}
\UnaryInfC{$\Phi$}

f:id:kivantium:20150407102721p:plain
\AxiomCには公理や前提となる命題を記述します。
\UnaryInfCには単一の命題からの帰結を記述します。

\AxiomC{$\Phi$}
\AxiomC{$\Psi$}
\BinaryInfC{$\Phi \land \Psi$}

f:id:kivantium:20150407103119p:plain
\BinaryInfCには2つの命題からの帰結を記述します。この命令を使うためには2つ以上の\AxiomCや\UnaryInfなどが必要です。
同様に\TrinaryInfCは3つの命題からの帰結を記述します。

\AxiomC{$\Phi$}
\AxiomC{$\Psi$}
\BinaryInfC{$\Phi \land \Psi$}
\AxiomC{$X \to \Upsilon$}
\BinaryInfC{$(\Phi \land \Psi) \land (X \to \Upsilon)$}

f:id:kivantium:20150407103538p:plain

\AxiomC{$\Gamma$}
\AxiomC{$[\Phi]_1$}
\BinaryInfC{$\Psi$}
\RightLabel{{\scriptsize 1}}
\UnaryInfC{$\Phi \to \Psi$}

f:id:kivantium:20150408111232p:plain

\RightLabel命令で線に番号をつけます。

以上の命令を組み合わせることで複雑な証明図を書くことができます。

Peter Smith's documentationの説明が詳しいので参考にしてください。