在节点之间和之后添加信息

Question 1

您提到了使用替代包的可能性。您还提到了沿线某处有一片森林。也许如果您只见树木不见森林，那么您应该画一片森林。

此解决方案基于当前版本的森林derivation tree。我根据您当前的代码定义了一种样式。它还定义了circular empty nodes仅指示forest为空节点绘制圆圈的样式。我认为将其与的代码分开可能会很有用derivation tree。

除了可以用来格式化树的各种键之外森林包中，你可以使用蒂克兹样式fork label并rule label确定推理规则标签的格式：

\tikzset{
  fork label/.style={},
  rule label/.style={},
}

rule label影响不分支的规则。fork label影响分支的规则。

这些对应两个森林键，fork label可rule label用于指定树中分支和非分支规则的标签。fork label是自定义的森林选项：

declare autowrapped toks={fork label}{},

用于指定边缘路径：

      edge path={
        \noexpand\path [\forestoption{edge}] (!u.parent anchor) -- +(0,-20pt) node [midway, anchor=west, right, fork label] {$\forestoption{fork label}$} -| (.child anchor)\forestoption{edge label};
      },

这里第一次出现的fork label是 TikZ 样式。第二次出现的是\forestoption{fork label}。rule label不需要自定义选项，因为我们可以使用现有选项，只需创建一个森林风格：

    rule label/.style={
      edge label={node [pos=.5, right, anchor=west, rule label] {$##1$}},
    },

rule label和都将其内容包装在数学环境中，因此在这些情况下fork label不需要符号。 $...$

此外，left label将在左侧格式化节点标签。right label将在右侧格式化节点标签。我应该指出，从技术上讲，这些不是节点标签。事实上，它们是树中的附加节点：

    left label/.style={
      before typesetting nodes={
        insert before={[{##1}, no edge, before drawing tree={x+=7.5pt}]}
      }
    },
    right label/.style={
      before typesetting nodes={
        insert after={[{##1}, no edge, before drawing tree={x-=7.5pt}]}
      }
    },

我这样做是为了森林而不是根据树中节点的内容计算适当的兄弟间距。这样，树就会根据其内容适当地间隔，而希望在指定树时不需要太多干预。

要使用derivation tree和circular empty nodes样式，只需将它们放入环境的前言中forest：

\begin{forest}
  derivation tree,
  circular empty nodes,

这将适当地格式化树并启用附加选项和样式。然后您可以说，例如：

  [, left label={$p,q\lor \lnot p$},
    [, fork label=\lor L, right label={$\lnot p$}
      [, rule label=\lor R, left label={$p$}
      ]
    ]
    [, left label={$q$}
    ]
  ]
\end{forest}

生产：

这大大简化了树的规范并使其更容易从源代码读取。

对原始代码进行翻译后，发现其中附加的节点为红色，结果如下：

完整代码：

\documentclass[tikz,border=10pt,multi]{standalone}
\usepackage{forest}
\tikzset{
  fork label/.style={},
  rule label/.style={},
}
\forestset{
  derivation tree/.style={
    declare autowrapped toks={fork label}{},
    for tree={
      l sep+=15pt,
      edge path={
        \noexpand\path [\forestoption{edge}] (!u.parent anchor) -- +(0,-20pt) node [midway, anchor=west, right, fork label] {$\forestoption{fork label}$} -| (.child anchor)\forestoption{edge label};
      },
      parent anchor=south,
      child anchor=north,
      if level=0{}{
        if={equal(n_children("!u"),1)}{
          before packing={calign with current}
        }{
          if n=1{
            before packing={
              !u.calign primary child/.wrap pgfmath arg={##1}{n}
            }
          }{
            before packing={
              !u.calign secondary child/.wrap pgfmath arg={##1}{n}
            }
          }
        }
      }
    },
    rule label/.style={
      edge label={node [pos=.5, right, anchor=west, rule label] {$##1$}},
    },
    left label/.style={
      before typesetting nodes={
        insert before={[{##1}, no edge, before drawing tree={x+=7.5pt}]}
      }
    },
    right label/.style={
      before typesetting nodes={
        insert after={[{##1}, no edge, before drawing tree={x-=7.5pt}]}
      }
    },
    before packing={
      for tree={
        tier/.wrap pgfmath arg={tier ##1}{level},
      }
    }
  },
  circular empty nodes/.style={
    before typesetting nodes={
      for tree={
        if content={}{circle, draw, anchor=center, inner sep=0pt, minimum size=5pt}{}
      }
    },
  }
}
\begin{document}
\begin{forest}
  derivation tree,
  circular empty nodes,
%   /tikz/rule label/.style={text=blue, font=\bfseries\small},
  /tikz/fork label/.style={red},
  [, label=left:{$(\lnot(p\land(q\lor\lnot r)))\leftrightarrow s,p\rightarrow (q\land r)$},
      [, left label={$p\land r$},
          [, left label={$q,r$}, rule label=\land L,
              [, left label={$\lnot(p\land(q\lor\lnot r)),s$},
                [, right label={$p\land(q\lor\lnot r)$}, rule label=\lnot L,
                    [, right label={$p$}
                    ]
                  [, right label={$\circ q\lor\lnot r$}, fork label=\land R
                      [, right label={$q,\lnot r$}, rule label=\lor R,
                      ]
                  ]
                ]
              ]
              [, right label={$\lnot(p\land(q\lor\lnot r)),s$}, fork label=\leftrightarrow L
                  [, left label={$p\land(q\lor\lnot r)$}, rule label=\lnot R,
                      [, left label={$p,q\lor\lnot r$}, rule label=\land L,
                          [, left label={$q$},
                          ]
                          [, left label={$\lnot r$}, fork label=\lor L
                              [, right label={$r$}, rule label=\lnot R,
                              ]
                          ]
                      ]
                  ]
              ]
          ]
        ]
        [, right label={$p$}, fork label=\rightarrow L
          [, left label={$s,\lnot(p\land(q\lor\lnot r))$},
                [, right label={$p\land(q\lor\lnot r)$}, rule label=\lnot L,
                    [, right label={$p$},
                    ]
                    [, right label={$p\lor\lnot r$}, fork label=\lor R
                        [, right label={$q,\lnot r$}, rule label=\lor R,
                            [, left label={$r$}, rule label=\lnot R,
                            ]
                        ]
                    ]
                ]
            ]
            [, right label={$\lnot(p\land(q\lor\lnot r)),s$}, fork label=\leftrightarrow L
                [, left label={$p\land(q\lor\lnot r)$}, rule label=\lnot R,
                    [, left label={$p,q\lor\lnot r$}, rule label=\land L,
                    ]
                ]
            ]
        ]
    ]
\end{forest}
\end{document}

如果您愿意，您还可以配置样式，以便left label使用right label数学模式或提供在左侧和右侧指定推导规则的选项。当然，这些可能性是否对您有用则完全是另一回事。

Answer