☰

prooftrees.sty：我怎样才能对单个表达式而不是整行进行编号？

tag-icon • tag-icon forest trees logic proof-package
prooftrees.sty：我怎样才能对单个表达式而不是整行进行编号？

使用 prooftrees.sty (https://ctan.org/pkg/prooftrees)，是否有一个选项或技巧可以获得不同于默认的行号方案？

我想格式化与输出匹配的真值树https://www.umsu.de/logik/trees/（直接链接到示例：https://www.umsu.de/logik/trees/?f=(p\lor%20(q\land%20r))\to%20((p\lor%20q)\land%20(p\lor%20r))）。

唯一相关的区别是，在 prooftrees 中，分支规则产生的任何两个新表达式都标有相同的行号，而 umsu.de 则按照某些逻辑教科书，分配两个不同的“行”号（或者说“表达式”号）。此外，应该可以为单个表达式分配复选标记，而不是全部分配给行（行可能包含任意数量的不同表达式，通常只标记其中一个）。

我确实意识到行号会受到插入的影响move by=1，但是分支规则产生的表达式不再处于相同的水平位置。

答案1

如果prooftrees增加检查线而不是 wffs。然而，它并没有这样做。检查是通过以下方式添加的：

content+'={\ \forestregister{check with}#1},

或者

+content'={\forestregister{check with}#1\ },

取决于检查是向左还是向右。无论哪种方式，这都是在操纵包含 wff 的节点的内容。这构成整行的唯一情况是 wff 构成整行。

虽然我不能排除我做了一些奇怪的事情，但目前我看不出我是如何引入所描述的错误：这部分代码非常简单。它所做的只是操纵节点内容，即附加或添加到特定的 wff。因此，据我所知，除非我看到相反的例子，否则我prooftrees不会犯这样的错误。

我相信有很多其他错误，所以如果你想报告其中一个，请这样做。我只是对这个特定错误的存在表示怀疑。

prooftrees没有提供绘制链接中所示类型的表的选项。这些树没有展示prooftrees旨在解决的问题，因此该包在这里与此无关。基本上，它们的结构就像语言学家的树一样：一切都与 wff 相符 - 数字、wff、对齐、检查等。这里您所需要的只是一个语言学家的树绘制包，只需将所有内容放入节点中即可。

例如，您可以直接使用forest，它是 的基数prooftrees。这样，​​您就不会使用某些东西来尝试解决您没有的问题。

你可以以相同的方式使用prooftrees，只需关闭编号和对齐即可。然而，这实际上只是增加了另一层代码，只会减慢编译速度而毫无用处。

所以我只会forest在这里使用。

toks例如，这里您真正需要的只是一些自定义和样式。

\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}

产生了一个语言学家友好的画面：

语言学家友好的画面

唯一的缺点是，实际上，失去了用于证明理由的交叉引用。如果您需要，可以从 借用代码prooftrees。但是，在这里使用它的理由较少，因为不需要移动东西，因此自动化的优势较少。还是有一些优势的，但它们可能不值得这么麻烦。

相关内容