summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/prftree
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2014-12-02 00:55:36 +0000
committerKarl Berry <karl@freefriends.org>2014-12-02 00:55:36 +0000
commitab4c97bb1913e7167819b3e3c2688a0e5200f011 (patch)
tree3a92d1b788fa89ea4c49b249e57e80162208cb55 /Master/texmf-dist/doc/latex/prftree
parent5a51ac01bebab92f1bb7e8f4091a423e5ac6905d (diff)
prftree (1dec14)
git-svn-id: svn://tug.org/texlive/trunk@35712 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc/latex/prftree')
-rw-r--r--Master/texmf-dist/doc/latex/prftree/README9
-rw-r--r--Master/texmf-dist/doc/latex/prftree/prftreedoc.pdfbin0 -> 267456 bytes
-rw-r--r--Master/texmf-dist/doc/latex/prftree/prftreedoc.tex1721
3 files changed, 1730 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/prftree/README b/Master/texmf-dist/doc/latex/prftree/README
new file mode 100644
index 00000000000..5c6a8ef263c
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/prftree/README
@@ -0,0 +1,9 @@
+The prftree package provides a package to write proof trees for
+natural deduction calculi, sequent-like calculi, and similar.
+
+The package is composed by the filed
+- prftree.sty: containing the LaTeX engine to typeset proof trees;
+- prftreedoc.pdf: the human readable documentation for the package;
+- prftreedoc.tex: the source code for the documentation.
+
+The package is distributed under the GNU General Public License.
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
new file mode 100644
index 00000000000..ce700a53cce
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
new file mode 100644
index 00000000000..8af679ea760
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
@@ -0,0 +1,1721 @@
+\documentclass{amsart}
+\usepackage[ND,SEQ]{prftree}
+\usepackage{url}
+
+\setlength{\fboxsep}{0pt}
+
+\begin{document}
+\title{Proof Trees in \LaTeX}
+\date{}
+\author{Marco Benini}
+\address{Dipartimento di Scienza e Alta Tecnologia\\
+ Universit\`a degli Studi dell'Insubria\\
+ via Valleggio 11, I-22100 Como, Italy}
+\email{marco.benini@uninsubria.it}
+\urladdr{http://marcobenini.wordpress.com}
+\maketitle
+
+% --------------------------
+
+\section{Introduction}\label{sec:introduction}
+Writing proofs in natural deduction or in similar, tree-like calculi,
+is always a challenge: from the typographical point of view, these
+proofs are complex objects that cannot be simply typeset using the
+standard \LaTeX{} commands. Thus, many packages have been developed:
+Sam Buss's \texttt{bussproofs.sty},
+\url{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}; Makoto
+Tatsuta's \texttt{proof.sty},
+\url{http://research.nii.ac.jp/~tatsuta/proof-sty.html}; and
+\texttt{prooftree.sty} by Paul Taylor,
+\url{http://mirror.ctan.org/macros/generic/proofs/taylor}.
+
+All these packages have their merits and weaknesses. For example,
+Buss's package is extremely flexible but inference rules with more
+than five assumptions cannot be directly typeset. On the other hand,
+Tatsuta's package provides a very simple set of commands doing a
+fine job, but customisation is very limited. Taylor's package provides
+a natural syntax for writing proofs, but customisation is limited, and
+the package has an expire date.
+
+The package presented in the following provides most of the features
+which are already present in Buss's package, coupled with some new
+ones. This package uses a syntax which is closer to Tatsuta's one, but
+almost all the typesetting process is parametric, so that each bit of
+a proof can be customised at will.
+
+The graphical appearance of a proof is similar to the one obtained
+using Taylor's package, but the additional features allow to set up
+the graphical output to follow the style of some of the standard
+textbooks, e.g., A.S.~Troelstra and H.~Schwichtenberg, \textit{Basic
+ Proof Theory}, Cambridge University Press (2000).
+
+% --------------------------
+\clearpage
+\section{Basic Commands}\label{sec:basic_commands}
+The package is invoked by putting \verb|\usepackage{prfree.sty}| in
+the preamble of the document, and installation reduces to put the file
+\texttt{prftree.sty} somewhere in the \LaTeX{} search
+path.\vspace{2ex}
+
+A proof tree constructs a box with the following internal structure:
+\begin{center}
+ {\setlength{\unitlength}{1em}
+ \begin{picture}(31,6)
+ \put(7,4){\framebox(17,2){$\mbox{assumption}_1 \cdots
+ \mbox{assumption}_n$}}
+ \put(6,3){\line(1,0){19}}
+ \put(26,2){\framebox(5,2){rule name}}
+ \put(0,2){\framebox(5,2){label}}
+ \put(10,0){\framebox(11,2){conclusion}}
+ \end{picture}}
+\end{center}
+In turn, each assumption is typeset as a box which has usually the
+shape of another proof tree, while the rule name and the label are
+typeset in a text box, and the conclusion in a math box. The aspect of
+the proof line is controlled by suitable options, as is the presence
+of the rule name and of the label. Options cover other aspects of the
+graphical rendering of a proof tree, as it will be explained
+later. The basic command to build a proof tree is \verb|\prftree|.
+
+For example, the proof of $A \supset \neg\neg A$ in natural deduction
+is:
+\begin{displaymath}
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}
+This proof is generated by the following \LaTeX{} code:
+\begin{verbatim}
+ \begin{displaymath}
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+ \end{displaymath}
+\end{verbatim}
+
+In general, the syntax of the \verb|\prftree| command is:
+\begin{displaymath}
+ \verb|\prftree|[\mbox{options}] \cdots
+ [\mbox{options}]\{\mbox{assumption}_1\} \cdots
+ \{\mbox{assumption}_n\}\{\mbox{conclusion}\}
+\end{displaymath}
+Assumptions are optional and there may be any number of them. Each
+assumption may contain a proof tree, which is typeset
+independently. The conclusion is mandatory, and it is supposed to be a
+formula. Assumptions and the conclusion are typeset in a display style
+math environment. Options control the way the proof is generated: in
+the example, the \verb|r| option has been used to signal that the
+first argument of \verb|\prftree| is the name of the inference rule.
+
+The available options are:
+\begin{itemize}
+\item\ [\textbf{r}], [\textbf{rule}], [\textbf{by rule}],
+ [\textbf{by}], [\textbf{right}]: the first argument after the
+ options is the rule name, which is typeset in text mode;
+\item\ [\textbf{l}], [\textbf{left}], [\textbf{label}]: the first
+ argument after the options is the label of the rule, which is
+ typeset in text mode. If a rule name is present, the first argument
+ is the rule name, and the second one is the label;
+\item\ [\textbf{straight}], [\textbf{straight line}],
+ [\textbf{straightline}]: makes the proof line solid;
+\item\ [\textbf{dotted}], [\textbf{dotted line}],
+ [\textbf{dottedline}]: makes the proof line dotted;
+\item\ [\textbf{dashed}], [\textbf{dashed line}],
+ [\textbf{dashedline}]: makes the proof line dashed;
+\item\ [\textbf{f}], [\textbf{fancy}], [\textbf{fancy line}],
+ [\textbf{fancyline}]: the proof line will be fancy;
+\item\ [\textbf{s}], [\textbf{single}], [\textbf{single line}],
+ [\textbf{singleline}]: makes the proof line single;
+\item\ [\textbf{d}], [\textbf{double}], [\textbf{double line}],
+ [\textbf{doubleline}]: makes the proof line double;
+\item\ [\textbf{noline}]: suppresses the proof line (prevails over all
+ other line options);
+\item\ [\textbf{summary}]: renders the proof line as the summary
+ symbol (prevails over all other line options except \textbf{noline}).
+\end{itemize}
+By default the proof line is straight and single. Options may be
+written in sequence, as in \verb|[r,f,d]|, which means that the proof
+tree will have a rule name, and the proof line will be fancy and
+double, or separately, as in \verb|[r][f][d]|, or even as a
+combination, like \verb|[r][f,d]|. Options are evaluated
+left-to-right, so \verb|[d,s]| is the same as \verb|[s]|, while
+\verb|[noline,straight,d]| is the same as \verb|[noline]|.
+
+The conjunction introduction rule illustrates the various line
+options\footnote{The reader is invited to look at the source code of
+ the documentation to see how these examples have been implemented.}:
+\begin{displaymath}
+ \begin{array}{lcc@{\qquad}l}
+ \mbox{default (single straight)} &
+ \prftree{A}{B}{A \wedge B} &
+ \prftree[r]{$\wedge$I}{A}{B}{A \wedge B} &
+ \texttt{[straight]} \\
+ \mbox{double straight} &
+ \prftree[d]{A}{B}{A \wedge B} &
+ \prftree[d,r]{$\wedge$I}{A}{B}{A \wedge B} &
+ \texttt{[double,straight]} \\
+ \mbox{single dotted} &
+ \prftree[dotted]{A}{B}{A \wedge B} &
+ \prftree[dotted,r]{$\wedge$I}{A}{B}{A \wedge B} &
+ \texttt{[dotted]} \\
+ \mbox{double dotted} &
+ \prftree[dotted,d]{A}{B}{A \wedge B} &
+ \prftree[dotted,d,r]{$\wedge$I}{A}{B}{A \wedge B} &
+ \texttt{[double,dotted]} \\
+ \mbox{single dashed} &
+ \prftree[dashed]{A}{B}{A \wedge B} &
+ \prftree[dashed,r]{$\wedge$I}{A}{B}{A \wedge B} &
+ \texttt{[dashed]} \\
+ \mbox{double dashed} &
+ \prftree[dashed,d]{A}{B}{A \wedge B} &
+ \prftree[dashed,d,r]{$\wedge$I}{A}{B}{A \wedge B} &
+ \texttt{[double,dashed]} \\
+ \mbox{single fancy} &
+ \prftree[f]{A}{B}{A \wedge B} &
+ \prftree[f,r]{$\wedge$I}{A}{B}{A \wedge B} &
+ \texttt{[fancy]} \\
+ \mbox{double fancy} &
+ \prftree[f,d]{A}{B}{A \wedge B} &
+ \prftree[f,d,r]{$\wedge$I}{A}{B}{A \wedge B} &
+ \texttt{[double,fancy]} \\
+ \mbox{noline} &
+ \prftree[noline]{A}{B}{A \wedge B} &
+ \prftree[noline,r]{$\wedge$I}{A}{B}{A \wedge B} &
+ \texttt{[noline]}
+ \end{array}
+\end{displaymath}\vspace{1ex}
+
+An assumption is a special proof tree, built by the command:
+\begin{displaymath}
+ \verb|\prfassumption|\{\text{formula}\}
+\end{displaymath}
+Similarly, a bounded assumption is produced by the command:
+\begin{displaymath}
+ \verb|\prfboundedassumption|\{\text{formula}\}
+\end{displaymath}
+as in the previous example.
+
+Although it is possible to type assumptions directly as argument of
+\verb|\prftree|, it is better to use the commands above: as explained
+later, since a proof tree is a box with an internal structure, the
+assumption commands take care of building this structure
+appropriately, while the direct typing does not, which may produce
+unexpected results.\vspace{2ex}
+
+Similarly, axioms are produced by the commands
+\begin{displaymath}
+ \verb|\prfaxiom|\{\mbox{axiom}\}
+\end{displaymath}
+and
+\begin{displaymath}
+ \verb|\prfbyaxiom|\{\mbox{name}\}\{\mbox{axiom}\}
+\end{displaymath}
+For example, the axiom stating that equality is reflexive, is
+\begin{displaymath}
+ \begin{array}{cc}
+ \prfaxiom{\forall x\, x = x} &
+ \prfbyaxiom{refl}{\forall x\, x = x}
+ \end{array}
+\end{displaymath}
+and they are generated by the \LaTeX{} code
+\begin{displaymath}
+ \begin{array}{cc}
+ \verb|\prfaxiom{\forall x\, x = x}|&
+ \verb|\prfbyaxiom{refl}{\forall x\, x = x}|
+ \end{array}
+\end{displaymath}\vspace{-.2ex}
+
+Finally, a proof summary is used to summarise a proof. The
+corresponding command is:
+\begin{displaymath}
+ \verb|\prfsummary|[\mbox{name}]\{\mbox{assumption}_1\} \cdots
+ \{\mbox{assumption}_n\}\{\mbox{conclusion}\}
+\end{displaymath}
+The name of the proof is optional, while the assumptions and the
+conclusion are treated as in \verb|\prftree|. When present, the proof
+name is typeset in text mode.
+
+For example, \verb|\prfsummary{\forall x\, x = x}| produces
+\begin{displaymath}
+ \prfsummary{\forall x\, x = x}
+\end{displaymath}
+while \verb|\prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}| gives
+\begin{displaymath}
+ \prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}
+\end{displaymath}\vspace{-.2ex}
+
+In general, a proof tree is a \TeX{} box containing all the pieces of
+the tree, with strict bounds: for example,
+\begin{displaymath}
+ \fbox{\prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}}
+\end{displaymath}
+
+% --------------------------
+\clearpage
+\section{Parameters}\label{sec:parameters}
+A number of parameters may be used to control the typesetting of proof
+trees. They may be changed globally or locally, following the usual
+scoping rules of \TeX{}. In this respect, remember that each
+assumption is typeset independently, so parameters may be changed on a
+sub-proof basis, as will be done in most examples.\vspace{2ex}
+
+There are various \TeX{} dimensions that influence how proofs are
+constructed:
+\begin{itemize}
+\item\ \verb|\prflinepad| (default 0.3ex): the space between the
+ bottom line of assumptions and the proof line, and also the space
+ between the proof line and the top of the conclusion;
+\item\ \verb|\prflineextra| (default 0.3em): the length which extends
+ on the left and on the right the proof line so that it is slightly
+ longer than the largest between the conclusion and the list of
+ (direct) assumptions;
+\item\ \verb|\prflinethickness| (default 0.2pt): the thickness of the
+ proof line;
+\item\ \verb|\prfemptylinethickness| (default 4 times the line
+ thickness): in the rare case when the line is empty, but there are
+ assumptions, this is the distance between the assumptions and the
+ conclusion;
+\item\ \verb|\prfrulenameskip| (default 0.2em): the space between the
+ proof line and the rule name;
+\item\ \verb|\prflabelskip| (default 0.2em): the space between the
+ proof label and the proof line;
+\item\ \verb|\prfinterspace| (default .6em): the space between two
+ subsequent assumptions in the assumption list;
+\item\ \verb|\prfdoublelineinterspace| (default 1.2pt): the space
+ between the two lines of a double line.
+\end{itemize}
+
+For example,
+\begin{displaymath}
+ \prflinepad=.7ex
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}
+is typeset by
+\begin{verbatim}
+ \prflinepad=.7ex
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{verbatim}
+
+Similarly, \verb|\prflineextra=-.4em| and \verb|\prfrulenameskip=.8em|
+produce:
+\begin{displaymath}
+ {\prflineextra=-.4em
+ \prfrulenameskip=.8em
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}}
+\end{displaymath}
+
+Also, \verb|\prflinethickness=3pt| and
+\verb|\prfdoublelineinterspace=2pt| in the upper sub-proof generate:
+\begin{displaymath}
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prflinethickness=3pt
+ \prfdoublelineinterspace=2pt
+ \prftree[r,d]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}
+The corresponding code is
+\begin{verbatim}
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prflinethickness=3pt
+ \prfdoublelineinterspace=2pt
+ \prftree[r,d]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{verbatim}
+
+Line thickness does not affect dashed, dotted, and fancy lines, but
+interline space does: in the example,
+\verb|\prfdoublelineinterspace=4pt| on a fancy line produces
+\begin{displaymath}
+ \prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prfdoublelineinterspace=4pt
+ \prftree[r,d,f]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}\vspace{.2ex}
+
+Fancy lines are drawn by the \verb|\prffancyline| command. This can be
+redefined: as a guideline, the package defines it as
+\begin{verbatim}
+ \def\prffancyline{\cleaders\hbox to .63em%
+ {\hss\raisebox{-.5ex}[.2ex][0pt]{$\sim$}\hss}\hfill}
+\end{verbatim}\vspace{2ex}
+
+Label spacing works exactly as rule name spacing. Actually, it is
+possible to have a proof with both a label and a rule name:
+\begin{displaymath}
+ \prftree[r]{$\supset$I}
+ {\prflabelskip=.7em
+ \prftree[r,l]{$\supset$I}
+ {[\textsl{$\bot\mathrm{E}$ will not work here!}]}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{displaymath}
+which has been typeset by
+\begin{verbatim}
+ \prftree[r]{$\supset$I}
+ {\prflabelskip=.7em
+ \prftree[r,l]{$\supset$I}
+ {[\textsl{$\bot\mathrm{E}$ will not work here!}]}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+\end{verbatim}\vspace{2ex}
+
+The \verb|\prfinterspace| controls the distance between
+assumptions. Specifically, this is the space between the \emph{boxes}
+containing two assumptions.
+
+Consider the following example
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfboundedassumption{A \rightarrow (B \rightarrow C)}}
+ {\prfboundedassumption{A}}
+ {B \rightarrow C}}
+ {\prftree
+ {\prfboundedassumption{A \rightarrow B}}
+ {\prfboundedassumption{A}}
+ {B}}
+ {C}}
+ {A \rightarrow C}}
+ {(A \rightarrow B) \rightarrow (A \rightarrow C)}}
+ {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B)
+ \rightarrow (A \rightarrow C))}
+\end{displaymath}
+Although the assumptions in the top line are well spaced, the two
+sub-proofs on the top are too close. This can be corrected in two
+different ways: by putting an explicit space, via \verb|\hspace|, in
+front of the second sub-proof, or after the first
+sub-proof---remember, they are just boxes
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfboundedassumption{A \rightarrow (B \rightarrow C)}}
+ {\prfboundedassumption{A}}
+ {B \rightarrow C}\hspace{1.5em}}
+ {\prftree
+ {\prfboundedassumption{A \rightarrow B}}
+ {\prfboundedassumption{A}}
+ {B}}
+ {C}}
+ {A \rightarrow C}}
+ {(A \rightarrow B) \rightarrow (A \rightarrow C)}}
+ {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B)
+ \rightarrow (A \rightarrow C))}
+\end{displaymath}
+otherwise, putting $\verb|\prfinterspace|=1.5\mathrm{em}$ before the
+sub-proof whose conclusion is $C$, one obtains the more pleasant
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prfinterspace=1.5em
+ \prftree
+ {\prftree
+ {\prfboundedassumption{A \rightarrow (B \rightarrow C)}}
+ {\prfboundedassumption{A}}
+ {B \rightarrow C}}
+ {\prftree
+ {\prfboundedassumption{A \rightarrow B}}
+ {\prfboundedassumption{A}}
+ {B}}
+ {C}}
+ {A \rightarrow C}}
+ {(A \rightarrow B) \rightarrow (A \rightarrow C)}}
+ {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B)
+ \rightarrow (A \rightarrow C))}
+\end{displaymath}\vspace{.2ex}
+
+The rendering of bounded assumptions is modified by
+\verb|\prfboundedstyle|. When $\verb|\prfboundedstyle| = 0$, the
+format of the assumption is $[\mbox{formula}]$, which is the default
+behaviour; with $\verb|\prfboundedstyle| = 1$, the formula is
+cancelled by a horizontal line; with $\verb|\prfboundedstyle| > 1$,
+the custom \verb|\prfdiscargedassumption| command is invoked:
+\begin{displaymath}
+ \begin{array}{c@{\qquad}c@{\qquad}c}
+ \prfboundedassumption{A(x)} &
+ {\prfboundedstyle=1\prfboundedassumption{A(x)}} &
+ {\prfboundedstyle=2\prfboundedassumption{A(x)}}
+ \end{array}
+\end{displaymath}
+
+The \verb|\prfdiscargedassumption| can be freely redefined. The
+package provides a reference implementation:
+\begin{verbatim}
+ \def\prfdiscargedassumption#1{\left\langle{#1}\right\rangle}
+\end{verbatim}\vspace{2ex}
+
+Proof summaries are drawn according to \verb|\prfsummarystyle|. The
+default value is $0$, which produces a vertical dotted line. Setting
+$\verb|\prfsummarystyle| = 1$ produces a huge $\Pi$, while
+$\verb|\prfsummarystyle| = 2$ produces a $\prod$. The value $3$ uses a
+$\mathcal{D}$ as the derivation symbol. Values greater than $3$ force
+the summary to be rendered by the \verb|\prffancysummarybox| command.
+\begin{displaymath}
+ \begin{array}{@{}c@{\quad}c@{\qquad}c@{\qquad}c@{}}
+ \verb|\prfsummarystyle| = 0 &
+ {\prfsummary{\forall x.\, x = x}} &
+ {\prfsummary{B(x)}{A(x)}} &
+ {\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge C(x)}} \\[2ex]
+ \verb|\prfsummarystyle| = 1 &
+ {\prfsummarystyle1\prfsummary{\forall x.\, x = x}} &
+ {\prfsummarystyle1\prfsummary{B(x)}{A(x)}} &
+ {\prfsummarystyle1\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge
+ C(x)}} \\[1ex]
+ \verb|\prfsummarystyle| = 2 &
+ {\prfsummarystyle2\prfsummary{\forall x.\, x = x}} &
+ {\prfsummarystyle2\prfsummary{B(x)}{A(x)}} &
+ {\prfsummarystyle2\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge
+ C(x)}} \\[1ex]
+ \verb|\prfsummarystyle| = 3 &
+ {\prfsummarystyle3\prfsummary{\forall x.\, x = x}} &
+ {\prfsummarystyle3\prfsummary{B(x)}{A(x)}} &
+ {\prfsummarystyle3\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge C(x)}}
+ \\[1ex]
+ \verb|\prfsummarystyle| = 4 &
+ {\prfsummarystyle4\prfsummary{\forall x.\, x = x}} &
+ {\prfsummarystyle4\prfsummary{B(x)}{A(x)}} &
+ {\prfsummarystyle4\prfsummary[name]{A(y)}{D(x)}{B(x) \wedge C(x)}}
+ \end{array}
+\end{displaymath}
+
+The fancy summary box is composed by the \verb|\prffancysummarybox|
+command. This can be modified at will. The package defines it as
+\begin{verbatim}
+ \newbox\prf@@fancysummarybox\newdimen\prf@@fancysymmarylen
+ \def\prffancysummarybox{%
+ \sbox{\prf@@fancysummarybox}{\Huge$\bigtriangledown$}%
+ \prf@@fancysymmarylen\ht\prf@@fancysummarybox%
+ \advance\prf@@fancysymmarylen\dp\prf@@fancysummarybox%
+ \sbox{\prf@@fancysummarybox}{%
+ \raisebox{.25\prf@@fancysymmarylen}[.8\prf@@fancysymmarylen]%
+ [0pt]{\usebox{\prf@@fancysummarybox}}}%
+ \prf@@fancysymmarylen\wd\prf@summary@label%
+ \ifdim\prf@@fancysymmarylen>\z@\relax%
+ \prf@@fancysymmarylen\wd\prf@@fancysummarybox%
+ \wd\prf@summary@label.4em%
+ \hbox to\prf@@fancysymmarylen{%
+ \usebox\prf@@fancysummarybox}\kern-.4em%
+ \box\prf@summary@label%
+ \else\usebox\prf@@fancysummarybox\fi}
+\end{verbatim}\vspace{2ex}
+
+The assumptions, conclusions, labels, and rule names are drawn using
+the following commands, which may be redefined:
+\begin{verbatim}
+ \def\prfConclusionBox#1{\hbox%
+ {$\displaystyle\begingroup#1\endgroup\mathstrut$}}
+ \def\prfAssumptionBox#1{\hbox%
+ {$\displaystyle\begingroup#1\endgroup\mathstrut$}}
+ \def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup\strut}}
+ \def\prfLabelBox#1{\hbox{\begingroup#1\endgroup\strut}}
+\end{verbatim}
+It is not advisable to change these commands in a radical way, unless
+one understands how the graphical engine works.
+
+% -------------------------------------
+\clearpage
+\section{Labels and References}\label{sec:references}
+As discharged assumptions are often hard to track in a proof, the
+package provides a mechanism to label them and to reference them
+inside a proof tree. A reference is made up of three pieces: the
+\emph{label}, which is the name to denote the reference inside the
+text, the \emph{reference value}, which is the value denoted by the
+label, and the \emph{anchor}, which is the graphical rendering of the
+value aside the labelled point of the proof.
+
+For example,
+\begin{displaymath}
+ \begin{prooftree}
+ \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$}
+ {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption<assum:A>{A}}
+ {\prfboundedassumption<assum:not_A>{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+ \end{prooftree}
+\end{displaymath}
+is generated by the following code
+\begin{verbatim}
+ \begin{prooftree}
+ \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$}
+ {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption<assum:A>{A}}
+ {\prfboundedassumption<assum:not_A>{\neg A}}
+ {\bot}}
+ {\neg\neg A}}
+ {A \supset \neg\neg A}
+ \end{prooftree}
+\end{verbatim}
+The labels are \verb|assum:A| and \verb|assum:not_A|, the reference
+values are $1$ and $2$, respectively, and the anchors are these values
+on the discharged assumptions on the top of the proof. The references
+to these labels are the values in the rule names.\vspace{2ex}
+
+The \verb|prooftree| environment delimits the scope of labels: the
+\verb|\end{prooftree}| declaration makes the labels still available
+for reference, but numbering of new labels will restart from
+$1$. Enclosing a proof tree in a \verb|prooftree| environment is not
+mandatory: in such case, labels will be global to the
+document.\vspace{2ex}
+
+Sometimes, labels require two compilation steps to be correctly
+generated: in fact, as \LaTeX{} labels, forward references may be
+undefined in the first compilation step. The package issues a warning
+in this case, and display a \verb|??| for the invalid reference. Also,
+notice how the assumption reference mechanism is analogous to \LaTeX{}
+labels, but it is independent from it.\vspace{2ex}
+
+A reference to a label is made by the
+$\verb|\prfref|\langle\mathrm{label}\rangle$ command: its argument is
+a label, i.e., a string of text following the same rules as the
+argument of the \LaTeX{} \verb|\label| command. As in the \verb|\ref|
+command, the resulting value has no formatting.\vspace{2ex}
+
+A labelled assumption is generated by the following commands:
+\begin{displaymath}
+ \begin{array}{l}
+ \verb|\prfassumption|\langle[\mathrm{option}]\mathrm{label}\rangle
+ \{\mathrm{assumption}\}
+ \\
+ \verb|\prfboundedassumption|\langle[\mathrm{option}]
+ \mathrm{label}\rangle\{\mathrm{assumption}\}
+ \end{array}
+\end{displaymath}
+The first one acts as \verb|\prfassumption| but also declares the
+assumption label and decorates the assumption text with the
+anchor. The second one does the same on bounded assumptions.
+
+The generation of labels is controlled by the option value:
+\begin{itemize}
+\item \textbf{n}, \textbf{number}, \textbf{arabic}: generates a number
+ (default);
+\item \textbf{r}, \textbf{roman}: generates a lowercase roman number;
+\item \textbf{R}, \textbf{Roman}: generates an uppercase
+ roman number;
+\item \textbf{a}, \textbf{alph}, \textbf{alpha}, \textbf{alphabetic}:
+ produces a lowercase letter;
+\item \textbf{A}, \textbf{Alph}, \textbf{Alpha}, \textbf{Alphabetic}:
+ produces an uppercase letter;
+\item \textbf{f}, \textbf{s}, \textbf{function}, \textbf{symbol},
+ \textbf{function symbol}: produces a footnote symbol, as in
+ Section~C.8.4 of Lamport's, \textit{\LaTeX: A document preparation
+ system};
+\item \textbf{l}, \textbf{label}: tells that the label has not to be
+ defined. This is used to generate a labelled assumption sharing the
+ label with another one, which declares the value and the format.
+\end{itemize}
+Except for \textbf{l} and \textbf{label}, all the options are used to
+format the anchor following the standard \LaTeX{} way available for
+counters. No multiple options are allowed.
+
+For example, the disjunction elimination rule is a perfect way to
+illustrate the reason behind the \textbf{label} option, i.e., the need
+to discharge a pair of assumptions:
+\begin{displaymath}
+ \begin{prooftree}
+ \prfinterspace=1.2em
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:orE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orE>{B}}{C}}{C}
+ \end{prooftree}
+\end{displaymath}
+\begin{verbatim}
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:orE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orE>{B}}{C}}{C}
+\end{verbatim}
+
+If a label is declared more than once, a warning is issued when the
+\textbf{label} option is not used: although this is not a mistake, it
+may indicate that a label is reused when it should not.
+
+The same example can be used to show how the other options work:
+\begin{displaymath}
+ \begin{array}{ccc}
+ \begin{prooftree}
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEn>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[n]assum:orEn>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEn>{B}}{C}}
+ {C}
+ \end{prooftree} &
+ \begin{prooftree}
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEr>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[r]assum:orEr>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEr>{B}}{C}}
+ {C}
+ \end{prooftree} &
+ \begin{prooftree}
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orER>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[R]assum:orER>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orER>{B}}{C}}
+ {C}
+ \end{prooftree} \\
+ \begin{prooftree}
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEa>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[a]assum:orEa>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEa>{B}}{C}}
+ {C}
+ \end{prooftree} &
+ \begin{prooftree}
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEA>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[A]assum:orEA>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEA>{B}}{C}}
+ {C}
+ \end{prooftree} &
+ \begin{prooftree}
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEf>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[f]assum:orEf>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEf>{B}}{C}}
+ {C}
+ \end{prooftree}
+ \end{array}
+\end{displaymath}
+
+Also, as the \verb|\prfboundedstyle| varies, the resulting proof trees
+are:
+\begin{displaymath}
+ \begin{array}{ccc}
+ \begin{prooftree}
+ \prfboundedstyle=0
+ \prfsummarystyle=4
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:AorE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:AorE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:AorE>{B}}{C}}
+ {C}
+ \end{prooftree} &
+ \begin{prooftree}
+ \prfboundedstyle=1
+ \prfsummarystyle=4
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:BorE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:BorE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:BorE>{B}}{C}}
+ {C}
+ \end{prooftree} &
+ \begin{prooftree}
+ \prfboundedstyle=2
+ \prfsummarystyle=4
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:CorE>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<assum:CorE>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:CorE>{B}}{C}}
+ {C}
+ \end{prooftree}
+ \end{array}
+\end{displaymath}\vspace{.2ex}
+
+The \verb|prfassumptioncounter| is the \LaTeX{} counter used to
+generate the assumption values. It contains the last used value, and
+initially, it is set to $0$. By modifying its value, e.g., to
+\verb|\setcounter{prfassumptioncounter}{1}|,
+\begin{displaymath}
+ \begin{prooftree}
+ \setcounter{prfassumptioncounter}{1}
+ \prfsummarystyle=2
+ \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEff>}$}
+ {\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[f]assum:orEff>{A}}{C}}
+ {\prfsummary{\Gamma,
+ \prfboundedassumption<[l]assum:orEff>{B}}{C}}
+ {C}
+ \end{prooftree}
+\end{displaymath}\vspace{.2ex}
+
+A labelled assumption box is graphically constructed by the package
+command \verb|\prflabelledassumptionbox| which can be redefined if
+needed. It takes two arguments: the assumption and the anchor. Its
+standard definition is
+\begin{verbatim}
+ \def\prflabelledassumptionbox#1#2{%
+ \setbox\prf@fancybox\hbox{${#1}$}%
+ \prf@tmp\wd\prf@fancybox%
+ \setbox\prf@fancybox\hbox{$\box\prf@fancybox^{#2}$}%
+ \wd\prf@fancybox\prf@tmp%
+ \prf@assumption{\box\prf@fancybox}}
+\end{verbatim}
+
+Moreover, also a labelled and bounded assumption is graphically
+rendered by the same command. There is just one exception: when
+$\verb|\prfboundedstyle| > 1$. In fact, since that style is
+controlled by a command that can be redefined, the same must hold for
+references in that style. The command which is called in this case is
+\verb|\prflabelleddiscargedassumption| which can be redefined if
+needed; its standard definition in the package is
+\begin{verbatim}
+ \def\prflabelleddiscargedassumption#1#2{%
+ \prflabelledassumptionbox{\left\langle{#1}\right\rangle}{#2}}
+\end{verbatim}\vspace{2ex}
+
+Also proof summaries can be labelled and referenced. The syntax
+extends the \verb|\prfsummary| command:
+\begin{displaymath}
+ \verb|\prfsummary|\langle[\mathrm{option}]\mathrm{label}\rangle
+ [\mathrm{name}]\{\mathrm{assumption}1\} \cdots
+ \{\mathrm{assumption}_n\}\{\mathrm{conclusion}\}
+\end{displaymath}
+The reference argument works in the same way as the corresponding one
+for assumptions, and the options are the same.
+
+\begin{displaymath}
+ \setcounter{prfsummarycounter}{0}
+ \begin{array}{c@{\qquad}c@{\qquad}c@{\qquad}c@{\qquad}c}
+ {\prfsummarystyle=0
+ \prfsummary<proof:a0>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<proof:a1>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=2
+ \prfsummary<proof:a2>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=3
+ \prfsummary<proof:a3>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=4
+ \prfsummary<proof:a4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{displaymath}
+
+These examples have been generated by the following code snippet:
+\begin{verbatim}
+ {\prfsummarystyle=X
+ \prfsummary<proof:aX>{A}{B}{A \wedge B}}
+\end{verbatim}
+
+The \verb|[option]| part of the label specification is optional, and
+it works exactly as the option field of labelled assumptions. This is
+best illustrated by an example:
+\begin{displaymath}
+ \setcounter{prfsummarycounter}{0}
+ \begin{array}{cccc}
+ {\prfsummarystyle=1
+ \prfsummary<[r]proof:b1>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[R]proof:b2>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[f]proof:b3>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[a]proof:b4>{A}{B}{A \wedge B}} \\ &
+ {\prfsummarystyle=1
+ \prfsummary<[A]proof:b5>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ \end{array}
+\end{displaymath}
+
+These examples have been generated by the following code snippet:
+\begin{verbatim}
+ {\prfsummarystyle=1
+ \prfsummary<[r]proof:bX>{A}{B}{A \wedge B}}
+\end{verbatim}
+and the last line uses the \verb|label| option.\vspace{2ex}
+
+The value of the summary labelling is controlled by the
+\verb|prfsummarycounter| counter, which is initially $0$ and contains
+the last used value.
+
+% -------------------------------------
+\clearpage
+\section{Simplified Commands}\label{sec:simplified_commands}
+The basic commands illustrated so far allow to control proof trees in
+all aspects, but they tend to be verbose in practise. Thus, a number
+of abbreviations are provided to make handier the writing of proofs.
+
+Since they may collide with other packages, these macros are activated
+by suitable options. By loading the package as
+\verb|\usepackage[ND]{prftree.sty}|, the following abbreviations are
+available, which correspond to the inference rule of natural deduction
+calculi:
+\begin{itemize}
+\item \verb|\NDA|: assumption;
+\item \verb|\NDAL|: labelled assumption;
+\item \verb|\NDD|: bounded assumption;
+\item \verb|\NDDL|: labelled bounded assumption;
+\item \verb|\NDP|: generic proof tree;
+\item \verb|\NDANDI|: conjunction introduction;
+\item \verb|\NDANDER|: conjunction elimination, right;
+\item \verb|\NDANDEL|: conjunction elimination, left;
+\item \verb|\NDANDE|: conjunction elimination, unspecified;
+\item \verb|\NDIMPI|: implication introduction;
+\item \verb|\NDIMPIL|: implication introduction with the label of the
+ discharged assumption;
+\item \verb|\NDIMPE|: implication elimination;
+\item \verb|\NDORIR|: disjunction introduction, right;
+\item \verb|\NDORIL|: disjunction introduction, left;
+\item \verb|\NDORI|: disjunction introduction, unspecified;
+\item \verb|\NDORE|: disjunction elimination;
+\item \verb|\NDOREL|: disjunction elimination with the label of the
+ discharged assumptions;
+\item \verb|\NDALLI|: universal quantifier introduction;
+\item \verb|\NDALLE|: universal quantifier elimination;
+\item \verb|\NDEXI|: existential quantifier introduction;
+\item \verb|\NDEXE|: existential quantifier elimination;
+\item \verb|\NDEXE|: existential quantifier elimination with the label
+ of the discharged assumption;
+\item \verb|\NDTI|: truth introduction;
+\item \verb|\NDFE|: falsity elimination;
+\item \verb|\NDLEM|: Law of Excluded Middle.
+\end{itemize}
+
+For example, the proof
+\begin{displaymath}
+ \begin{prooftree}
+ \NDOREL{simp:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]simp:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{simp:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{simp:notnotA}{\neg\neg A}}
+ {\NDDL{simp:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prooftree}
+\end{displaymath}
+is typeset in abbreviated form by the following code
+\begin{verbatim}
+ \NDOREL{simp:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]simp:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{simp:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{simp:notnotA}{\neg\neg A}}
+ {\NDDL{simp:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{verbatim}\vspace{2ex}
+
+Similarly, by loading the package as
+\verb|\usepackage[SEQ]{prooftree.sty}|, the following abbreviations
+are available, which roughly correspond to the inference rule of
+sequent calculi:
+\begin{itemize}
+\item \verb|\SEQA|: assumption;
+\item \verb|\SEQD|: bounded assumption;
+\item \verb|\SEQP|: generic proof;
+\item \verb|\SEQAX|: axiom rule;
+\item \verb|\SEQLF|: left falsity;
+\item \verb|\SEQLW|: left weakening;
+\item \verb|\SEQRW|: right weakening;
+\item \verb|\SEQLC|: left contraction;
+\item \verb|\SEQRC|: right contraction;
+\item \verb|\SEQLAND|: left conjunction;
+\item \verb|\SEQRAND|: right conjunction;
+\item \verb|\SEQLOR|: left disjunction;
+\item \verb|\SEQROR|: right disjunction;
+\item \verb|\SEQLIMP|: left implication;
+\item \verb|\SEQRIMP|: right implication;
+\item \verb|\SEQLALL|: left universal quantification;
+\item \verb|\SEQRALL|: right universal quantification;
+\item \verb|\SEQLEX|: left existential quantification;
+\item \verb|\SEQREX|: right existential quantification;
+\item \verb|\SEQCUT|: cut rule.
+\end{itemize}
+
+One can load the package with both options at the same
+time.\vspace{2ex}
+
+Since the implication symbol is usually represented either as
+$\rightarrow$ or as $\supset$, the package allows to choose which
+representation to use. By default, implication is $\rightarrow$, but
+loading the package with the \verb|[IMP]| option switches to
+$\supset$. The same effect is obtained by the commands
+\verb|\prfIMPOptiontrue| (implication is $\supset$) and
+\verb|prfIMPOptionfalse| (implication is $\rightarrow$).
+
+Of course, the reader is encouraged to develop her own abbreviations
+starting from the provided ones.
+
+% -------------------------------------
+\clearpage
+\section{Hints and Tricks}\label{sec:hints_and_tricks}
+This section shows a few hints and tricks to use the package at its
+best.\vspace{2ex}
+
+Consider the proof:
+\begin{displaymath}
+ \begin{prooftree}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{a:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prooftree}
+\end{displaymath}
+the space between the axiom and the sub-proof of the positive case is
+visually much less than the space between the positive and the
+negative cases. Looking at boxes, the space is exactly the same, but
+the perception is that spacing is wrong.
+
+We can correct this perception in two distinct ways: by adding space
+between the axiom and the positive case; or, conversely, by moving the
+negative case closer to the positive one.
+
+The first strategy yields:
+\begin{displaymath}
+ \begin{prooftree}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}\hspace{.8em}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prooftree}
+\end{displaymath}
+and this effect is given by adding an appropriate \verb|\hspace| after
+the axiom, as in
+\begin{verbatim}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}\hspace{.4em}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{verbatim}
+
+Adding the same space in front of the positive case is equivalent.
+
+The second strategy yields:
+\begin{displaymath}
+ \begin{prooftree}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-.4em}\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prooftree}
+\end{displaymath}
+Again, this is obtained by adding a negative \verb|hspace| after the
+positive case, or, equivalently, before the negative one:
+\begin{verbatim}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-.8em}\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{verbatim}
+
+In general, to make a wide proof \emph{compact}, one can appropriately
+add negative spaces in front of sub-proofs so to make them closer and
+letting them to overlap as boxes, but not visually, thus \emph{tiling}
+the space.\vspace{2ex}
+
+Since proof trees are boxes, it is easy to align them on need. For
+example the following proof tree, with the bounding box put in
+evidence
+\begin{displaymath}
+ \fbox{\prfsummarystyle=1
+ \prfsummary{A}{B}{A \wedge B}}
+\end{displaymath}
+can be used wherever a box may appear. In the flow of text, it will
+look like \fbox{\prfsummarystyle=1\prfsummary{A}{B}{A \wedge B}}, so
+that the conclusion is aligned with the baseline. This makes easier to
+align proof trees, as in
+\begin{center}
+ \fbox{\prfsummarystyle=1
+ \prfsummary{f}{g}{f \wedge g}}\qquad
+ \fbox{$\begin{prooftree}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-.4em}\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+ \end{prooftree}$}
+\end{center}
+since this is the natural way to put proofs side by side:
+\begin{verbatim}
+ \fbox{\prfsummarystyle=1
+ \prfsummary{f}{g}{f \wedge g}}\qquad
+ \fbox{$
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\hspace{-.4em}\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}$}
+\end{verbatim}
+
+But, if really one has to include a proof tree in the flow of text, it
+is slightly better to vertically centre the box, as in
+\fbox{$\vcenter{\prfsummary{A}{B}{A \wedge B}}$}. This is obtained by
+\begin{verbatim}
+ $\vcenter{\prfsummary{A}{B}{A \wedge B}}$
+\end{verbatim}
+
+Of course, the result is not pleasant, because rows are far apart,
+which is unavoidable because of the height of the proof tree. The
+same principle applies also to arrays of proof trees:
+\begin{displaymath}
+ \begin{array}{lcccc}
+ \text{some text} &
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{displaymath}
+\begin{verbatim}
+ \begin{array}{lcccc}
+ \text{some text} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ {\prfsummarystyle=1
+ \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{verbatim}
+vertically aligns the cells to their baselines.
+
+On the contrary
+\begin{displaymath}
+ \begin{array}{lcccc}
+ \text{some text} &
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{displaymath}
+is much better, and it is obtained by
+\begin{verbatim}
+ \begin{array}{lcccc}
+ \text{some text} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b1>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b2>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b3>{A}{B}{A \wedge B}} &
+ \vcenter{\prfsummarystyle=1
+ \prfsummary<[l]proof:b4>{A}{B}{A \wedge B}}
+ \end{array}
+\end{verbatim}\vspace{2ex}
+
+The labelling of proof summaries is useful when a proof is very large
+and there is the need to split it. The strategy is to select some
+sub-proofs and to show them as summaries: instead of writing
+\begin{displaymath}
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
+ {\NDIMPIL{a:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]a:notnotA}{\neg\neg A}}
+ {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{displaymath}
+we may consider to define
+\begin{displaymath}
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ \mbox{Let }
+ \vcenter{\vbox{\prfsummary<s:abbrev>
+ {\NDDL{s:notnotA}{\neg\neg A}}
+ {\NDAL{s:notA}{\neg A}}
+ {\neg\neg A \supset A}}}
+ \equiv
+ \vcenter{\hbox{$\NDIMPIL{s:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}}
+ {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}$}}
+\end{displaymath}
+allowing to abbreviate the whole proof as
+\begin{displaymath}
+ \NDOREL{s:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]s:notA}{A}}{\neg\neg A \supset A}}
+ {\prfsummary<s:abbrev>
+ {\NDDL{[l]s:notnotA}{\neg\neg A}}
+ {\NDDL{[l]s:notA}{\neg A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{displaymath}
+
+The corresponding \LaTeX{} code is
+\begin{verbatim}
+ \setcounter{prfsummarycounter}{0}
+ \setcounter{prfassumptioncounter}{0}
+ \mbox{Let }
+ \vcenter{\vbox{\prfsummary<s:abbrev>
+ {\NDDL{s:notnotA}{\neg\neg A}}
+ {\NDAL{s:notA}{\neg A}}
+ {\neg\neg A \supset A}}}
+ \equiv
+ \vcenter{\hbox{$\NDIMPIL{s:notnotA}
+ {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}}
+ {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}}
+ {\neg\neg A \supset A}$}}
+\end{verbatim}
+for the definition of the proof summary, and
+\begin{verbatim}
+ \NDOREL{s:notA}{\NDLEM{A \vee \neg A}}
+ {\NDIMPI{\NDDL{[l]s:notA}{A}}{\neg\neg A \supset A}}
+ {\prfsummary<s:abbrev>
+ {\NDDL{[l]s:notnotA}{\neg\neg A}}
+ {\NDDL{[l]s:notA}{\neg A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{verbatim}
+for its use.
+
+% -------------------------------------
+\clearpage
+\section{More Examples}\label{sec:examples}
+This section shows a number of examples illustrating the package. See
+the previous sections for the description of the features.\vspace{2ex}
+
+The disjunction elimination rule, with various line options:
+\begin{displaymath}
+ \begin{array}{@{}ccc@{}}
+ {\prfsummarystyle=1
+ \prftree{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[d]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r][d]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l][d]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[dotted]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[d,dotted]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r,d,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l,d,dotted]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[dashed]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[d,dashed]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[d,r,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[d,l,dashed]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[f]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[r,f]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[l,f]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} \\
+ {\prfsummarystyle=1
+ \prftree[noline]{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[noline][r]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}} &
+ {\prfsummarystyle=1
+ \prftree[noline][l]{$\vee$E}{\prfsummary{\Gamma}{A \vee B}}
+ {\prfsummary{\Gamma, \prfboundedassumption{A}}{C}}
+ {\prfsummary{\Gamma, \prfboundedassumption{B}}{C}}
+ {C}}
+ \end{array}
+\end{displaymath}
+
+Proof that the Law of Excluded middle implies $\neg\neg A \supset A$:
+\begin{displaymath}
+ \prftree[r]{$\vee$E}
+ {\prfbyaxiom{LEM}
+ {A \vee \neg A}\hspace{.4em}}
+ {\prftree[r]{$\supset$I}
+ {\prfboundedassumption{A}}
+ {\neg\neg A \supset A}}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\bot$E}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{\neg\neg A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{displaymath}
+
+Proof that the Law of Excluded middle implies $\neg\neg A \supset A$
+with labels instead of rule names, except on axioms:
+\begin{displaymath}
+ \prftree[l]{$\vee$E}
+ {\prfbyaxiom{LEM}
+ {A \vee \neg A}\hspace{.6em}}
+ {\prftree[l]{$\supset$I}
+ {\prfboundedassumption{A}}
+ {\neg\neg A \supset A}}
+ {\prftree[l]{$\supset$I}
+ {\prftree[l]{$\bot$E}
+ {\prftree[l]{$\supset$E}
+ {\prfboundedassumption{\neg\neg A}}
+ {\prfboundedassumption{\neg A}}
+ {\bot}}
+ {A}}
+ {\neg\neg A \supset A}}
+ {\neg\neg A \supset A}
+\end{displaymath}
+
+Another simple proof in natural deduction:
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfboundedassumption{A \rightarrow (B \rightarrow C)}}
+ {\prfboundedassumption{A}}
+ {B \rightarrow C}\hspace{2em}}
+ {\prftree
+ {\prfboundedassumption{A \rightarrow B}}
+ {\prfboundedassumption{A}}
+ {B}}
+ {C}}
+ {A \rightarrow C}}
+ {(A \rightarrow B) \rightarrow (A \rightarrow C)}}
+ {(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B)
+ \rightarrow (A \rightarrow C))}
+\end{displaymath}
+
+The same proof, under the proposition-as-types interpretation:
+\begin{displaymath}
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfassumption{u\colon A \rightarrow (B \rightarrow C)}}
+ {\prfassumption{w\colon A}}
+ {u w\colon B \rightarrow C}\hspace{2em}}
+ {\prftree
+ {\prfassumption{v\colon A \rightarrow B}}
+ {\prfassumption{w\colon A}}
+ {v w\colon B}}
+ {u w(v w)\colon C}}
+ {\lambda w.\, u w(v w)\colon A \rightarrow C}}
+ {\lambda v w.\, u w(v w)\colon (A \rightarrow B) \rightarrow (A
+ \rightarrow C)}}
+ {\lambda u v w.\, u w(v w)\colon (A \rightarrow (B \rightarrow C))
+ \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))}
+\end{displaymath}
+
+A deduction in a sequent calculus:
+\begin{displaymath}
+ \prfinterspace=1.2em
+ \prftree
+ {\prftree
+ {\prftree
+ {\prftree
+ {\prfassumption{A \Rightarrow A}}
+ {\prftree
+ {\prfassumption{A \Rightarrow A}}
+ {\prftree
+ {B \Rightarrow B}
+ {C \Rightarrow C}
+ {B, B \rightarrow C \Rightarrow C}}
+ {A, A \rightarrow B, B \rightarrow C \Rightarrow C}}
+ {A, A \rightarrow B, A \rightarrow (B \rightarrow C)
+ \Rightarrow C}}
+ {A \rightarrow B, A \rightarrow (B \rightarrow C) \Rightarrow A
+ \rightarrow C}}
+ {A \rightarrow (B \rightarrow C) \Rightarrow (A \rightarrow B)
+ \rightarrow (A \rightarrow C)}}
+ {\Rightarrow (A \rightarrow (B \rightarrow C)) \rightarrow ((A
+ \rightarrow B) \rightarrow (A \rightarrow C))}
+\end{displaymath}
+
+% -------------------------------------
+\clearpage
+\section{Internals}\label{sec:internals}
+A proof tree is typeset as a \TeX{} box in horizontal mode. This means
+that wherever a character can stay, so does a proof: in principle,
+there is no need to put the proof in a math environment. Also, the
+width of a proof is exactly the width of the box; the height of the
+proof is the height of the conclusion plus the total height of all the
+matter above it; the depth of the proof is the depth of the
+conclusion. The proof is aligned so that the current baseline is the
+baseline of the conclusion.
+
+For example, the proof of $g \supset \neg\neg g$ in natural deduction
+is:
+\begin{displaymath}
+ \mbox{proof} \equiv
+ \fbox{\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$I}
+ {\prftree[r]{$\supset$E}
+ {\prfboundedassumption{g}}
+ {\prfboundedassumption{\neg g}}
+ {\bot}}
+ {\neg\neg g}}
+ {g \supset \neg\neg g}}
+\end{displaymath}
+The proof has been surrounded by a framebox to make evident its
+bounds. Also, since the letter $g$ has a depth, the example shows how
+depth in the conclusion influences the alignment of the proof with
+respect to the preceding text.\vspace{2ex}
+
+Actually, the fundamental command in the package is \verb|\prftree|:
+the commands to construct assumptions (\verb|\prfassumption| and
+\verb|\prfboundedassumption|), those to generate axioms
+(\verb|\prfaxiom| and \verb|\prfbyaxiom|), and \verb|\prfsummary| are
+just appropriate instances.\vspace{2ex}
+
+The \verb|\prftree| command is composed by a parser, which takes care
+of reading the various options and parameters, and by a graphical
+engine, \verb|\prf@draw|, which calculates and draw the box containing
+the proof tree.
+
+It may be useful to understand how the graphical engine works. In the
+first place, each proof tree is a box with a structure:
+\begin{center}
+ {\setlength{\unitlength}{1em}
+ \begin{picture}(27,6)
+ \put(0.8,0){\framebox(26.2,6){}}
+ \put(5,4){\framebox(18,1.8){$\cdots$}}
+ \put(5.2,4.2){\framebox(6,1.4){$\mbox{assumption}_1$}}
+ \put(16.8,4.2){\framebox(6,1.4){$\mbox{assumption}_n$}}
+ \put(7,3){\line(1,0){14}}
+ \put(22,2.3){\framebox(4.8,1.4){rule name}}
+ \put(1,2.3){\framebox(4.8,1.4){label}}
+ \put(8.5,0.2){\framebox(11,1.8){conclusion}}
+ \end{picture}}
+\end{center}
+
+The conclusion, the proof line, and the \emph{assumption line} are
+centred. The assumption line is the line whose first element is the
+conclusion of the first assumption, and whose last element is the
+conclusion of the last assumption, properly spaced so that all the
+assumptions fit in between. The width of the proof line is calculated
+as the maximum of the width of the assumption line and the conclusion,
+with the rule name and the label, if present, hanging on the right and
+the left, respectively.
+
+To calculate the assumption line, the engine keeps track of the
+position of the conclusion within a proof tree, which reduces to
+remember how far is the conclusion from the left margin
+(\verb|Lassum|), and how far it is from the right margin
+(\verb|Rassum|). So, the assumption line starts from the value of
+\verb|Lassum| of the first assumption, and finishes at \verb|Rassum|
+of the last assumption.
+
+Thus, with these values it is not difficult to figure out the
+mathematics to place the various boxes around, so to combine them into
+a proof tree. This is exactly what the graphical engine does.
+
+Unfortunately, when one writes assumptions as simple formulae, without
+the \verb|\prfassumption| command, the corresponding \verb|Lassum| and
+\verb|Rassum| are not set to $0$, which is the right value. In fact,
+the recursive expansion of the \verb|\prf@draw| macro follows the
+\emph{natural} order in the construction of the proof box, which is
+extremely useful because it allows to locally modify parameters in
+sub-proofs; but this order conflicts with proper rendering of
+assumptions which are not proof trees.
+
+Also, the hints on how to put space between assumptions, see
+Section~\ref{sec:hints_and_tricks}, may have strange effects: if space
+is added in front of the first assumption or behind the last one, this
+space makes invalid the values of \verb|Lassum| and \verb|Rassum|,
+respectively, yielding hard to predict results.
+
+It is worth remarking that the mathematics of the graphical engine is
+sound, which means that zero or negative values for the various
+dimensions specified as parameters, or using \emph{bizarre} boxes in
+the fancy commands, yields the expected results, as far as boxes do
+not have parts which extends beyond the bounds.\vspace{2ex}
+
+The implementation of references mimics the implementation of
+\verb|\label| and \verb|\ref| in \LaTeX. Whenever a reference is
+defined, through a command with the $\langle \mathrm{label}\rangle$ as
+the first argument, the reference value is created according to the
+options, and it gets stored in the \texttt{.aux} file, by writing
+$\verb|\prfauxvalue|\{\mathrm{label}\}\{\mathrm{value}\}$ in the
+file. Then, when the source code will be recompiled, and the
+\texttt{.aux} file read, this command will be executed before any
+occurrence of a reference, which can be resolved.
+
+Most difficulties in the implementation of references lie in the way
+to construct the boxes to be used in the proof tree. But, the tricky
+part is the interaction with the \LaTeX{} and \TeX{} kernel for error
+reporting. Actually, it is in this part that the bugs signalled in the
+next section have their origin.
+
+% -------------------------------------
+\clearpage
+\section{Future Features and Bugs}\label{sec:future_features}
+Essentially, all the features of Buss's package have been implemented
+but one: alignment of proofs according to the $\vdash$ (or equivalent)
+sign. While this feature is occasionally useful in the writing of
+sequent proofs, it requires some trickery in the graphical engine, so
+it has been postponed for the moment.\vspace{2ex}
+
+Moreover, automatic compact proofs have been analysed, but not
+implemented. A compact proof minimises the amount of space between
+subsequent assumptions, eventually making the upper trees to overlap
+as boxes, but not as typed text.
+
+The algorithm to obtain this result is not immediate: one should keep
+track of the left and right \emph{skylines} of a proof. Comparing the
+left skyline of an assumption with the right skyline of the next one,
+one can calculate what is the distance between the boxes so that the
+distance between the closest points in the skylines is exactly
+\verb|\prfinterspace|.
+
+It is not simple to code such an algorithm in \TeX{}, but the real
+difficulty is how to represent skylines and how to store them, since
+\TeX{} provides no abstract data structures. Hence, the implementation
+of this feature has been postponed to a remote future, or to the will
+of a real \TeX{} magician.\vspace{2ex}
+
+There are three bugs in the packages.
+
+The first one is that \verb|\mathrm| and similar may break a proof
+tree when used in the rule name. I have not been able to track down
+why this happens. The effect is that the proof tree is correctly
+constructed but it cannot be used as a box, e.g., it cannot be put
+inside a \verb|\fbox| or used in normal text. Although disappointing
+this bug can be easily circumvented by typesetting the proof tree in a
+math environment, e.g., by putting it into a math display or by
+enclosing it in a pair of dollar signs.\vspace{2ex}
+
+The second bug is minimal and in a future version it could be
+solved. If one considers the following proof:
+\begin{displaymath}
+ \begin{prooftree}
+ \fbox{%
+ \prflineextra=0pt
+ \prftree
+ {\prftree
+ {\prftree
+ {\prfboundedassumption{\neg\neg A}}
+ {\prfboundedassumption<bug:1>{\neg A}}
+ {\bot}}
+ {A}}
+ {\neg\neg A \supset A}}
+ \end{prooftree}
+\end{displaymath}
+the anchor of assumption (\prfref<bug:1>) is out of the bounding
+box. Usually, this is not a problem and, in case, it can be manually
+corrected
+\begin{displaymath}
+ \begin{prooftree}
+ \fbox{%
+ \prflineextra=0pt
+ \hbox{\prftree
+ {\prftree
+ {\prftree
+ {\prfboundedassumption{\neg\neg A}}
+ {\prfboundedassumption<[l]bug:1>{\neg A}}
+ {\bot}}
+ {A}}
+ {\neg\neg A \supset A}\hspace{.34em}}}
+ \end{prooftree}
+\end{displaymath}
+as in the following code:
+\begin{verbatim}
+ \prfassumption{\prftree{\prftree{\prftree
+ {\prfboundedassumption{\neg\neg A}}
+ {\prfboundedassumption<bug:1>{\neg A}}{\bot}}
+ {A}}{\neg\neg A \supset A}\hspace{.34em}}}
+\end{verbatim}\vspace{2ex}
+
+The third bug happens the first time a reference is created: if it is
+referred by \verb|\prfref| in the rule name, a strange ``immediate''
+follows it. This is not a problem, since the code has to be recompiled
+anyway to complete the definition of references, and this is enough to
+make the problem to disappear. Since it is a transient problem, I have
+not investigated any further.
+
+\vfill
+
+\end{document}