diff options
Diffstat (limited to 'Master/texmf-dist/doc/latex/prftree/prftreedoc.tex')
| -rw-r--r-- | Master/texmf-dist/doc/latex/prftree/prftreedoc.tex | 1721 |
1 files changed, 1721 insertions, 0 deletions
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} |