2

I am looking at different options to typeset proof trees. I have asked a more general question and run into some issues. In particular I am trying to understand how to display very large proof trees, maybe with hundreds of nodes. I am trying different combinations of packages bussproofs, ebproofs or tikz's library tree, and standalone or preview

In some cases the final proof tree is cropped, unless I set a large value for a border parameter. Issue (and question) is that I should not need to know such a value in advance. I do not understand why (it seems that) for some of those combinations I need to set it in advance.

Let me show my examples.

bussproofs + standalone. Output is cropped, unless I do not set a larger third (right) border parameter. If this could work, it would be the best settings for my little project. So the main question is: which piece of code I need to let pdf/latex to calculate the value to display a given proof tree in a large enough .pdf (.ps, .dvi) file?

\documentclass[border={10pt 50pt 50pt 50pt},varwidth]{standalone}
\usepackage{bussproofs}
\begin{document}
\begin{prooftree}
\AxiomC{A}
\UnaryInfC{B}
\AxiomC{C}
\BinaryInfC{D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{J}
\AxiomC{A}
\UnaryInfC{B}
\AxiomC{C}
\BinaryInfC{D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{J}
\BinaryInfC{JJ}
\AxiomC{A}
\UnaryInfC{B}
\AxiomC{C}
\BinaryInfC{D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{J}
\AxiomC{A}
\UnaryInfC{B}
\AxiomC{C}
\BinaryInfC{D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{J}
\BinaryInfC{JJ}
\BinaryInfC{JJJ}
% for a larger proof tree
% repeat all node as above, 
% and add a further line:  \BinaryInfC{JJJJ}
\end{prooftree}
\end{document}

bussproofs + preview. Output is cropped, unless I do not increase third (right) border parameter:

\documentclass[14pt]{article}
\usepackage{bussproofs}
\usepackage[active,tightpage]{preview}
\PreviewEnvironment{prooftree}
\renewcommand\PreviewBbAdjust{-10pt -10pt 50pt 10pt}
\begin{document}
\begin{prooftree}
   AS ABOVE, CUT AND PASTE FROM ABOVE
\end{prooftree}
\end{document}

ebproofs + standalone. Output is cropped, unless I do not increase third (right) border parameter from 10 to, say, 100:

\documentclass[border={10pt 10pt 10pt, 10pt},varwidth]{standalone}
\usepackage{ebproof}
\begin{document}
\begin{prooftree}
      AS BELOW, CUT AND PASTE FROM BELOW
\end{prooftree}
\end{document}

ebproofs + preview. Output is fine! This setting works. My question is: why so?

\documentclass[14pt]{article}
\usepackage{ebproof}
\usepackage[active,tightpage]{preview}
\PreviewEnvironment{prooftree}
\renewcommand\PreviewBbAdjust{-10pt -10pt 10pt 10pt}
\begin{document}
\begin{prooftree}
\hypo{ &\vdash A, B, C }
\infer1{ A &\vdash B, C }
\hypo{ D &\vdash E }
\infer2{ A, B, D &\vdash C, E }
\infer1{ A &\vdash B, C, D, E }
\hypo{ D &\vdash E }
\infer2{ A, B, D &\vdash C, E }
\hypo{ D &\vdash E  }
\infer2{ A, B, D &\vdash C, E }
\hypo{ D &\vdash E  }
\infer2{ A, B, D &\vdash C, E }
\hypo{ D &\vdash E  }
\infer2{ A, B, D &\vdash C, E }
\hypo{ D &\vdash E  }
\infer2{ A, B, D &\vdash C, E }
\hypo{ D &\vdash E  }
\infer2{ A, B, D &\vdash C, E }
\hypo{ D &\vdash E, 002 }
\infer2{ A, B, D &\vdash C, E, 002 }
\end{prooftree}
\end{document}

tikz + preview. Output is fine!, but I do not know whether there is a way to use tikz's tree library to define proof tree as in bussproofs/ebproofs (I suspect it is possible but it would need quite some work to be done)

\documentclass{article}
\usepackage{tikz}
\usepackage[active,tightpage]{preview}
\PreviewEnvironment{tikzpicture}
\usetikzlibrary{trees}
\begin{document}
\begin{tikzpicture}
    \node {root}
    [edge from parent fork down]
    child {node {left}}
    child {node {right}
        child[child anchor=north east] {node {AAA}}
        child {node {BBB}}
        [edge from parent fork down]
        child {node {BB0}}
        child {node {BB1}}
        [edge from parent fork down]
        child {node {BB0}}
        child {node {BB2}}
        [edge from parent fork down]
        child {node {BB0}}
        child {node {BB3}}
        %%%     REPEAT SEVERAL TIMES
        %%% [edge from parent fork down]
        %%%   child {node {BB0}}
        %%%   child {node {BBN}}
};
\end{tikzpicture}
\end{document}

---- EDIT

I got a comment from Emmanuel Beffara, who programmed ebproofs. I paste here with his permission.

> [...] Regarding the fact that bussproofs+preview fails, apparently that is because the prooftree environment in bussproofs produces its result in vertical mode with the current page width, so bounding box calculation fails. You can pacth your example as follows:

  \documentclass[12pt]{article}
  \usepackage{bussproofs}
  \usepackage[active,tightpage]{preview}
  \newenvironment{hproof}{}{\DisplayProof} % Just so we have an environment
  \PreviewEnvironment{hproof}
  \renewcommand\PreviewBbAdjust{-10pt -10pt 10pt 10pt}
  \begin{document}
  \begin{hproof}
    % Same contents as before
  \end{hproof}
  \end{document}

and it does work.

As to how to use TikZ trees to render proofs, I don't know if it practically feasible without much coding. At first I wanted to use TikZ to develop ebproof, because it would allow drawing over proofs and also rendering in very different styles, but I never found how to do the required placement operations within TikZ, in particular using a stack-based syntax, which is the only practical way of specifying complex proofs as far as I can tell.

  • 1
    It would be much more awkward to use TikZ's tree library here, even if it can be done. This certainly wouldn't be a convenient solution, especially if you need to draw a number of proofs like this. @marmot I assume the latter. – cfr Jul 6 '18 at 14:54
  • Is there a question here and, if so, what is it? – cfr Aug 27 '18 at 0:27
  • Passing 14pt to article gets you 10pt, by the way. – cfr Oct 3 at 16:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.