2

I want to draw things like

enter image description here

and optionally

enter image description here

I don't need to typeset proof trees as in the second picture, but it would be nice to know how to typeset it if anyone could do it without a sweat. But, I want to be able to draw the first picture with or without numbers on the left.

I found https://tex.stackexchange.com/a/244187/82730 and https://tex.stackexchange.com/a/242261/82730. But, the answers looked overly complex for a beginner. Also, I couldn't find prooftree package on CTAN.

5
  • For a TikZ solution look at the child action in the pgf manual (there is a whole section about trees) or the forest package which offers a convenient syntax. Have you tried something?
    – Bordaigorl
    Commented Jan 25, 2016 at 7:57
  • some other options: tex.stackexchange.com/questions/160325/…
    – Ignasi
    Commented Jan 25, 2016 at 9:34
  • prooftree package can be found in cfr's answer. Save this code in your working folder as prooftree.sty and test it.
    – Ignasi
    Commented Jan 25, 2016 at 9:36
  • @Bordaigorl I tried qtree and synttree. They all couldn't handle cramming multiple lines in one node. I will try others soon.
    – user82730
    Commented Jan 25, 2016 at 11:23
  • Let us continue this discussion in chat.
    – cfr
    Commented Jan 26, 2016 at 1:53

1 Answer 1

4

[Updated as a later version is now on CTAN. Note that most images were created with the early code and the spacing is a bit squashed. The current spacing is shown in the image illustrating the use of cross-references in justifications. This is because closure symbols are now properly accounted for when the tree is packed.]

I would use prooftrees. It goes without saying that I am biased. On the other hand, I would have happily not written this package if I could have found one which did the job I wanted.

The package is based on forest.

The package is a wrapper for forest. You set up the tree like this:

...
\usepackage{prooftrees}
...
\begin{prooftree}
  {
    <preamble, if any>
  }
  <tree specification in forest's bracket notation>
\end{prooftree}
...

The preamble may be empty, but the argument is mandatory. That is, you can have

\begin{prooftree}{}
  <tree>
\end{prooftree}

but not

\begin{prooftree}
  <tree>
\end{prooftree}

By default, lines are numbered on the left and levels are grouped when no branching occurs. In terms of the tree, this means that no line is drawn to the parent when there is only one child.

Some additional styles are available within the tree:

checked

marks a premise or sub-conclusion as discharged. By default, a tick is used, but this can be customised if required.

close

closes the branch. By default, \otimes is used, but this can be customised.

This means that you can say

\documentclass[tikz,border=10pt]{standalone}
\usepackage{prooftrees}% version 0.09
\begin{document}
\begin{prooftree}
  {
    close with={\ensuremath{\ast}}
  }
  [P \land (Q \lor \lnot R), checked
    [\lnot ((P \land Q) \land S), checked
      [\lnot (P \land S) \lor R, checked
        [\lnot\lnot S
          [P
            [Q \lor \lnot R, checked
              [\lnot (P \land Q), checked
                [\lnot P, close]
                [\lnot Q
                  [Q, close]
                  [\lnot R
                    [\lnot (P \land S), checked
                      [\lnot P, close]
                      [\lnot S, close]
                    ]
                    [R, close]
                  ]
                ]
              ]
              [\lnot S, close]
            ]
          ]
        ]
      ]
    ]
  ]
\end{prooftree}
\end{document}

to produce

proof tree

To put the line numbers in brackets and remove the dot, just do

\renewcommand*\linenumberstyle[1]{(#1)}

before drawing the tree

customised line numbering

Justifications for the inferences can be added using

just=<content>

For example

\renewcommand*\linenumberstyle[1]{(#1)}
\begin{prooftree}
  {
    close with={\ensuremath{\ast}},
  }
  [P \land (Q \lor \lnot R), checked
    [\lnot ((P \land Q) \land S), checked
      [\lnot (P \land S) \lor R, checked
        [\lnot\lnot S
          [P, just=from 1
            [Q \lor \lnot R, checked, just=from 1
              [\lnot (P \land Q), checked, just=from 2
                [\lnot P, close, just=from 7]
                [\lnot Q
                  [Q, close]
                  [\lnot R, just=from 6
                    [\lnot (P \land S), checked, just=from 3
                      [\lnot P, close, just=from 10]
                      [\lnot S, close]
                    ]
                    [R, close]
                  ]
                ]
              ]
              [\lnot S, close]
            ]
          ]
        ]
      ]
    ]
  ]
\end{prooftree}

These are aligned on the right as the line numbers are aligned on the left.

justifications

Cross-references are also supported following a : in the argument of just. By default, these are set to the left of justifications (for use with rule names), but this can be switched as below. References may use either the name of the node or a relative node name. For example:

\documentclass[tikz,multi,border=10pt]{standalone}
\usepackage{prooftrees,amsmath}
\begin{document}
\renewcommand*\linenumberstyle[1]{(#1)}
\begin{prooftree}
  {
    close with={\ensuremath{\ast}},
    just refs right
  }
  [P \land (Q \lor \lnot R), checked
    [\lnot ((P \land Q) \land S), checked
      [\lnot (P \land S) \lor R, checked
        [\lnot\lnot S
          [P, just=from:!r1
            [Q \lor \lnot R, checked, just=from:!r1, name=bert
              [\lnot (P \land Q), checked, just=from:!r11
                [\lnot P, close, just=from:!u]
                [\lnot Q
                  [Q, close]
                  [\lnot R, just=from:bert
                    [\lnot (P \land S), checked, just=from:!r111
                      [\lnot P, close, just=from:!u]
                      [\lnot S, close]
                    ]
                    [R, close]
                  ]
                ]
              ]
              [\lnot S, close]
            ]
          ]
        ]
      ]
    ]
  ]
\end{prooftree}
\end{document}

produces

cross-referenced nodes

The same system supports references in close if required.

to prove=<contents>

can be used in the preamble to provide a statement of the entailment or theorem to be proved. For example

\begin{prooftree}
  {
    close with={\ensuremath{\ast}},
    to prove={ \{P \land (Q \lor \lnot R), \lnot ((P \land Q) \land S), \lnot (P \land S) \lor R \} \sststile{L}{} \lnot S }
  }
...

produces

proof statement

It is also possible to move lines to later levels with or without justifications. Your samples don't seem to require these features, so they are not relevant here.

0

You must log in to answer this question.