LaTeXで証明木を書くためのおすすめパッケージ
目次:
普通の証明木(?)を書く
普通のproof treeは bussproofs
が良さげです。
- bussproof.sty:bussproofs: LaTeX proof tree style file
- マニュアル:http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/BussGuide2_Smith2012.pdf
- その他のスタイルも含め、詳しくはこちらを参照:
3. Natural deduction and sequent proofs - Logic MattersLogic Matters
TeX Live のパッケージ管理のコマンドtlmgr
を使って調べると以下のようになります。
$ tlmgr info bussproofs package: bussproofs category: Package shortdesc: Proof trees in the style of the sequent calculus longdesc: The package allows the construction of proof trees in the style of the sequent calculus and many other proof systems. One novel feature of the macros is they support the horizontal alignment according to some centre point specified with the command \fCenter. This is the style often used in sequent calculus proofs. The package works in a Plain TeX document, as well as in LaTeX; an exposition of the commands available is given in the package file itself. installed: Yes revision: 27488 sizes: run: 41k relocatable: No cat-version: 1.1 cat-date: 2016-06-24 19:18:15 +0200 cat-license: lppl1.3 cat-topics: maths proof cat-related: ebproof collection: collection-latexextra
証明木をflag notationで書く
読んでいた教科書が
Type Theory and Formal Proof: An Introduction
(https://www.amazon.co.jp/Type-Theory-Formal-Proof-Introduction/dp/110703650X)
というものだったのですが、本文中の旗記法(flag notation)を LaTeX で書くためのパッケージはないだろうかと探していたらありました。
flagderiv
というパッケージを入れればできるようです。
- flagderiv のサイト:CTAN: Package flagderiv
- マニュアル "The flagderiv package":http://mirror.hmc.edu/ctan/macros/latex/contrib/flagderiv/flagderiv.pdf
$ tlmgr info flagderiv package: flagderiv category: Package shortdesc: Flag style derivation package longdesc: The flagderiv package is used to create mathematical derivations using the flag/flagpole notation. The package features an intuitive command syntax, opening and closing multiple flagpoles, different comment styles, customizable symbols and label namespaces. installed: No sizes: src: 57k, doc: 213k, run: 9k relocatable: Yes cat-version: 0.10 cat-date: 2016-06-24 19:18:15 +0200 cat-license: gpl cat-topics: maths collection: collection-latexextra $ sudo tlmgr install flagderiv