So, I want to typeset some proof trees, i.e. trees of inference rules like those in natural deduction (see diagram below). Which are the best packages that you have found that allow you to do this, and which features do they have?
[Tex/LaTex] the best package out there to typeset proof trees
logicpackages
Related Solutions
Skipping over minor details, this may be accomplished with a tabular
:
\usepackage{array}
\newcolumntype{C}{>{$\displaystyle}c<{$}}
\newcommand{\onecol}[1]{\multicolumn{2}{C}{#1}}
The above code should go in the preamble. Then the big thing can be set by
\begin{figure}
\centering
\renewcommand{\arraystretch}{2} % adjust here for interrow spacing
\begin{tabular}{CC}
\onecol{Formula for first line} \\
\onecol{Formula for second line} \\
\onecol{Formula for third line} \\
Left formula & right formula (row 4)\\
Left formula & right formula (row 5)\\
...
\end{tabular}
\caption{Sequent calculus formulation}\label{fig:seqcalc}
\end{figure}
Instead of setting \arraystretch
you can define
\newcommand\mystrut{\vrule width 0pt height 24pt depth 24pt}
and insert \mystrut
in a cell in each row but the first and the last. Adjust the dimensions to suit.
Recently I have finished my thesis, and I added an appendix with some CINT (C/C++) code. I used listings
package, adding those lines on my preamble:
\definecolor{listinggray}{gray}{0.9}
\definecolor{lbcolor}{rgb}{0.9,0.9,0.9}
\lstset{
backgroundcolor=\color{lbcolor},
tabsize=4,
% rulecolor=,
language=[GNU]C++,
basicstyle=\scriptsize,
upquote=true,
aboveskip={1.5\baselineskip},
columns=fixed,
showstringspaces=false,
extendedchars=false,
breaklines=true,
prebreak = \raisebox{0ex}[0ex][0ex]{\ensuremath{\hookleftarrow}},
frame=single,
numbers=left,
showtabs=false,
showspaces=false,
showstringspaces=false,
identifierstyle=\ttfamily,
keywordstyle=\color[rgb]{0,0,1},
commentstyle=\color[rgb]{0.026,0.112,0.095},
stringstyle=\color[rgb]{0.627,0.126,0.941},
numberstyle=\color[rgb]{0.205, 0.142, 0.73},
% \lstdefinestyle{C++}{language=C++,style=numbers}’.
}
\lstset{
backgroundcolor=\color{lbcolor},
tabsize=4,
language=C++,
captionpos=b,
tabsize=3,
frame=lines,
numbers=left,
numberstyle=\tiny,
numbersep=5pt,
breaklines=true,
showstringspaces=false,
basicstyle=\footnotesize,
% identifierstyle=\color{magenta},
keywordstyle=\color[rgb]{0,0,1},
commentstyle=\color{Darkgreen},
stringstyle=\color{red}
}
The output I get looks like that:
Best Answer
Peter Smith's very useful LaTeX for Logicians page offers suggestions both for downward branching proof-trees and for natural deduction proofs in both Gentzen sequent-style (the tree-like style you seem to be after) and Fitch-style.
I've not used any of the alternatives for proof trees, as I use Fitch-style natural deduction proofs. But, I've found Smith a most reliable guide and for your desire he recommends as best of breed Sam Buss's
bussproofs.sty
. Smith also has remarks about a few other alternatives that you might want to check out.A quick example to produce your example tree would be: