LaTeXで証明木を書く

目次:

普通の証明木(?)を書く

普通のproof treeは bussproofs が良さげです。

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というパッケージを入れればできるようです。

$ 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