2

In this answer, user cfr offers the following code which gives output as in the following image:

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    for tree={math content},
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{##2.\quad ##1\quad ##3} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=15, close
  ]]]]]]]]]
\end{forest}
\end{document}

A proof tree where each node has a line number, a quad space, a formula, a quad space and a justification

I am wondering if anyone knows how to modify the code to produce output as in the following image:

A proof tree where the line numbers, formulas and justifications on branches are horizontally aligned One approach I can think of is storing the widths of each of the widest line number, formula, and justification along each branch, and then wrapping the content of each node on the branch in a three-column tabular where the column widths are fixed to these maximum widths. Then the position of the anchors of the nodes would be set to the north of the formula column so that the lines between branches are drawn to the centres of the formulas.

A significantly less elegant but much easier approach would be to have multiline tabulars containing all of the formulas on a branch (i.e. one for the formulas numbered 1, 2, 3; another for 4; another for 5, 8, 11; and so on). But I would like to avoid an approach like this which would require significant changes to the tree itself rather than its style.

Unfortunately I don't really have the technical expertise at present to even know where to start on actually implementing a more elegant solution, so I'd appreciate whatever help is on offer.

UPDATE

Here's a partial answer which involves processing the content into a one-line tabular with three columns, one for the line number, one for the wff and another for the justification:

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\usepackage{array}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{\begin{tabular}{>{\raggedleft}p{1em}cp{1em}}##2. & \ensuremath{##1} & \ensuremath{##3}\\\end{tabular}} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=1500, close
  ]]]]]]]]]
\end{forest}
\end{document}

The above makes it so that the centres of the formulas are horizontally aligned. Thus we obtain

aligned formula centres

instead of

misaligned formula centres

as in the original code. This already improves legibility and aesthetics.

The missing piece of the puzzle is to organise things such that the widths of the formula columns at 17. and 19. are set to the width of the formula column at 15. so that the line numbers and justifications are horizontally aligned as well. (And similarly throughout the tree.)

I think that this answer by cfr hints towards a way of calculating the width of each formula. But I don't know how to store the widths and then select the widest appropriate one for each set of formulas.

Another update

I created a fwidth tok that gets passed to the width of the formula column. Now everything is nicely aligned, but the trade-off is that the user needs to set this key for every node on the tree. The best way to find out what it should be set to is to plug the widest formula of a branch into the code

\newlength{\myl}
\settowidth{\myl}{formula goes here}
\the\myl

and then set fwidth to that length for every formula in the branch. See the example code below:

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb}
\usepackage{array}
\forestset{
  declare toks={from}{},
  declare toks={fwidth}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  Ow4 {content}{tempcounta}{from}{}{}{(##1)}{fwidth}{\begin{tabular}{p{1em}>{\centering\arraybackslash}p{##4}p{1em}}##2. & \ensuremath{##1} & \ensuremath{##3}\\\end{tabular}} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip}}{},
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r))), fwidth=158.8pt    
    [ (p\lor (q\land r)) , from=1, fwidth=158.8pt
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1, fwidth=158.8pt
        [ p , from=2, fwidth=5.1pt
          [ \lnot (p\lor q) , from=3, fwidth=35.5pt
            [ \lnot p , from=6, fwidth=35.5pt
              [ \lnot q , from=6, close, fwidth=35.5pt
          ]]]
          [ \lnot (p\lor r) , from=3, fwidth=35.5pt
            [1 \lnot p , from=7, fwidth=35.5pt
            [1 \lnot r , from=7, close, fwidth=35.5pt
        ]]]]
        [ (q\land r) , from=2, fwidth=28.6pt
          [1 q , from=5, fwidth=28.6pt
            [1 r , from=5, fwidth=28.6pt
              [1 \lnot (p\lor q) , from=3, fwidth=40.5pt
                [1 \lnot p , from=14, fwidth=40.5pt
                  [1 \lnot q , from=14, close, fwidth=40.5pt
              ]]]
              [1 \lnot (p\lor r) , from=3, fwidth=40.5pt
                [1 \lnot p , from=15, fwidth=40.5pt
                  [1 \lnot r , from=1500, close, fwidth=40.5pt
  ]]]]]]]]]
\end{forest}
\end{document}

Things look really nice now, but it would be considerably more convenient if fwidth could be calculated and set automatically. (It would also be nice to hide the overfull warnings that come from setting the line number and justification columns to a small fixed width.) I await someone with a deeper knowledge of TikZ and forest to show the way.

7
  • 1
    Here is a variant using tabulars, so that at least the three columns are aligned. Unfortunately anchoring the nodes to the north of the formula column, rather the node of the table, is just what I haven't been able to resolve. Nov 11, 2020 at 16:59
  • @lemontree Ah, I see we're basically trying to obtain the same output! As far as your solution with tabulars goes, have you tried setting the line number and justification columns to the same fixed width? I think this would make it so the middle of each tabular would then be the middle of the formula column.
    – solisoc
    Nov 12, 2020 at 3:44
  • This actually is a great idea; I just tried it and it worked. Thank you! If you post that as an answer to my question, I'll upvote and accept. Nov 12, 2020 at 12:28
  • @lemontree No problem! Glad I could help.
    – solisoc
    Nov 12, 2020 at 13:00
  • 1
    You can just use align=<tabular column specification> rather than \begin{tabular}... because forest's align is actually a tabular specification anyway.(align=c is making a single column tabular etc.)
    – cfr
    Nov 12, 2020 at 15:35

1 Answer 1

2

Here's a variation on the tabular/align idea which automatically determines the width of the central column (for the wff).

% ref.: https://tex.stackexchange.com/q/570449/

\documentclass[border=11pt]{standalone}
\usepackage[linguistics]{forest}
\usepackage{amsmath,amssymb,array}
\newcolumntype{C}[1]{>{\centering $}p{#1}<{$}}
\forestset{
  declare toks={from}{},
  declare toks register={claim},
  declare boolean={align me}{0},
  declare dimen={my width}{0pt},
  declare dimen register={lmeas},
  lmeas/.pgfmath=width("99."),
  declare dimen register={rmeas},
  rmeas/.pgfmath=width("(99)"),
  claim=,
  ll proof/.style={
    for tree={
      math content,
    },
    for root=align me,
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip},}{},
    for root={align me},
    where n children>=2{
      for children={align me}}{},
    before packing={
      tempcountb'=0,
      where align me={%
        tempcountb'+=1,
        tempdima/.max={>{OOw2+d}{max x}{min x}{##1-##2}}{%
          walk and save={temptoksa}{current,
             until={> O_=!{n children}{1}}{first,typeset node}}%
        },
        for nodewalk={load=temptoksa}{my width/.register=tempdima, typeset node}, 
      }{},
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        align=p{\foresteregister{lmeas}}C{\foresteoption{my width}}p{\foresteregister{rmeas}},
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{##2.\quad & ##1\quad & ##3} },
        typeset node,
      }
    },
    close/.style={label=below:\textsf{x}},
  },
}
\begin{document}
\begin{forest}
  ll proof,
  claim=\vdash ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))
  [ \lnot ((p\lor (q\land r))\to((p\lor q)\land (p\lor r)))    
    [ (p\lor (q\land r)) , from=1
      [ \lnot ((p\lor q)\land (p\lor r)) , from=1
        [ p , from=2
          [ \lnot (p\lor q) , from=3
            [ \lnot p , from=6
              [ \lnot q , from=6, close
          ]]]
          [ \lnot (p\lor r) , from=3
            [1 \lnot p , from=7
            [1 \lnot r , from=7, close
        ]]]]
        [ (q\land r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 \lnot (p\lor q) , from=3
                [1 \lnot p , from=14
                  [1 \lnot q , from=14, close
              ]]]
              [1 \lnot (p\lor r) , from=3
                [1 \lnot p , from=15
                  [1 \lnot r , from=15, close
  ]]]]]]]]]
\end{forest}
\end{document}

tableau-split-line-nos-with-alignment

Sašo could make this faster in any case, but I'm out of practice, so somebody else may be able to do better, too. The fancy column specifier seemed to get entangled with forest's parser. Hence the somewhat clunky approach. Like I say, somebody else will doubtless make it behave more politely.

2
  • Glorious, thank you. I'm excited to study how this works.
    – solisoc
    Nov 13, 2020 at 0:08
  • @solisoc I thought it would be enough to set the width of the middle column, but obviously that was a dumb assumption. You could get a slightly more compact tree by taking the maximum width of the wff numbers and justifications, but it didn't seem worth the trouble or compilation speed hit.
    – cfr
    Nov 13, 2020 at 0:19

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .