我正在寻找一种方法来制作一个有三列（行号、树本身和注释）的逻辑树。我尝试使用 tikz 矩阵，效果很好，但当我获得两个以上的分支时，边缘绘制命令就会停止工作，我必须手动绘制。有没有办法调整 tikz 中的列数？有没有我可以使用的其他包？
多谢
@Johannes_B，这是我目前拥有的代码
\documentclass{article}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{amsmath}
\usepackage{tikz}
\usepackage{tikz-qtree}
\begin{document}
\def\shoe{$\supset$}
\def\nee{$\mathord{\sim}$}
\def\nein{$\neg$}
\def\lub{$\lor$}
\noindent
\checkmark 1 \hspace{10ex} A \shoe B \hspace{8ex} (premise) \\
\checkmark 2 \hspace {10ex} B \shoe C \hspace{8ex} (premise) \\
\checkmark 3 \hspace{8.5ex} \nee(C \shoe A) \hspace{5.5ex} (conclusion) \\
\hspace{2ex} 4 \hspace{14ex} C \hspace{11ex} (3, \nee \shoe) \\ 5 \hspace{4.5ex}
\Tree [.{\nee A} [.{\nee B} {\nee A} {B} ] [.{C} {\nee A} {B} ]]
\hspace{4ex} (3, \nee \shoe) \\
6
\end{document}
或者
\documentclass{article}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{amsmath}
\usepackage{tikz}
\usetikzlibrary{matrix}
\begin{document}
\def\shoe{$\supset$}
\def\nee{$\mathord{\sim}$}
\def\nein{$\neg$}
\def\lub{$\lor$}
\begin{tikzpicture}
\matrix (m)[matrix of nodes, row sep=0.2em,
column sep=0.1em, text height=1.5ex, text depth=0.25ex]
{
1 & & A \shoe B & & (premise) \\
2 & & B \shoe C & & (premise) \\
3 & & \nee(C \shoe A) & & (conclusion) \\
4 & & C & & (3, \nee \shoe) \\
5 & & \nee A & & (3, \nee \shoe) \\ [2em]
6 & \nee B & & C & (3, \nee \shoe) \\ [2em]
7 & \nee A \hspace{0.5cm} B & & \nee A \hspace {0.5cm} B & (2, \shoe) \\ [2em]
};
\draw [-] (-3,3) -- (-0.5, 2);
\path[-] (m-5-3.south) edge (m-6-2.north)
(m-5-3.south) edge (m-6-4.north)
(m-6-2.south)
\end{tikzpicture}
\end{document}
问题是，当节点超过 2 个时，路径不再起作用，我必须手工绘制，这在我看来不是很高效
问题是，在下面的代码中，树在分支之前插入了一条垂直线。你们知道为什么吗？
\documentclass[tikz,border=5pt]{standalone}
\usepackage{forest}
\def\shoe{$\supset$}
\def\nee{$\mathord{\sim}$}
\def\nein{$\neg$}
\def\lub{$\lor$}
\begin{document}
\forestset{
ass/.append style={
before computing xy={l=\baselineskip},
no edge
},
}
\begin{forest}
for tree={
parent anchor=south,
child anchor=north,
align=center,
},
[(P \lub (G \& \nee D)) \& (P \shoe (\nee P \& (S \lub \nee Q), ass, name=n1
[P \lub (G \& \nee D),ass, name=n2
[P \shoe (\nee P \& (S \lub \nee Q)), ass, name=n3
[[P
[\hspace{0.005pt}, ass, name=n5
[\hspace{0.05pt}, ass, name=n6
[[\nee P, name=n7]
[\nee P \& (S \lub \nee G)
[\nee P, ass, name=n8
[S \lub \nee Q, ass, name=n9]]]]]]]
[G \& \nee D, name=n4
[G, ass
[\nee D, ass
[ [\nee P]
[\nee P \& (S \lub \nee G)
[\hspace{0.05pt}, ass
[\hspace{0.05pt}, ass
[\nee P, ass, name=n10
[S \lub \nee Q, ass, name=n11
[ [S,name=n12] [\nee Q]]]]]]]]]]]
]
]
]
]
\foreach \i in {1,...,12}
\node [xshift=-100pt, anchor=east] at (n\i -| n1) {\i.};
\foreach \i/\j in {2/{(1, \&)}}
\node [xshift=100pt, anchor=west] at (n\i -| n1) {\j};
\end{forest}
\end{document}
答案1
此软件包的更高版本现已在 CTAN 上 - 更新了答案以反映当前的使用情况等。
新答案 - 已更新
我终于受够了没有更好的解决方案可以提供给人们。逻辑不太适用，特别是在教授低年级课程时。
我的解决方案是使用新软件包。它肯定包含错误，并且并非完全自动化。但是，它比早期版本更加自动化，并且包含的错误至少比其中一些版本少。
买者自负...
该包名为prooftrees，并且依赖于forest。它定义了一个新环境prooftree，并为全局和本地配置提供了各种便利。它可以解决交叉引用、合并冲突的论证和移动行（有时自动；有时使用move by=<positive integer>）。行号和布局是自动的。为本地和全局配置提供了各种选项。
以下是使用交叉引用系统进行论证和推理的示例树。这既可以name用于命名 wff，也可以用于相对节点名称（如 Forest 所定义的那样），也可以混合使用。如果您不使用:，注释将按原样排版，因此您也可以just=From 2根据需要编写 或close={4,5}并放弃交叉引用支持。
\documentclass[tikz,border=5pt,multi]{standalone}
\usepackage{prooftrees}
\usepackage{amssymb}
\usepackage{mathtools,turnstile}
\begin{document}
\begin{prooftree}{}% default preamble - note this argument is REQUIRED
[P \vee (Q \vee \lnot R), grouped, just=Ass
[P \supset \lnot R, grouped, just=Ass
[Q \supset \lnot R, grouped, just=Ass
[\lnot\lnot R, grouped, just={Negated conclusion}, name=nc
[P, just={$\vee$ Elim:!r1}
[\lnot P, close={:!u,!c}
]
[\lnot R, close={:nc,!c}, just={$\supset$ Elim:!r11}
]
]
[Q \vee \lnot R
[Q, just={5 $\vee$ Elim:!u}
[\lnot Q, , close={:!u,!c}
]
[\lnot R, close={:nc,!c}, just={$\supset$ Elim:!r111}
]
]
[\lnot R, close={:nc,!c}
]
]
]
]
]
]
\end{prooftree}
\end{document}
这将生成一个带有行号和理由的证明树：
文档包含更多示例，包括一个工作示例，该示例解释了如何将树转换为森林括号符号，语言学家可能对此很熟悉，但我认为逻辑学家对此并不那么熟悉。（或者也许我只是过着过于受保护的生活。）
下面是文档中逐步执行的示例，其中包括使用来move by避免合并理由：
\documentclass[tikz,border=5pt,multi]{standalone}
\usepackage{prooftrees}
\usepackage{amssymb}
\usepackage{mathtools,turnstile}
\begin{document}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\newcommand*{\liff}{\ensuremath{\mathbin{\leftrightarrow}}}
\newcommand*{\elim}{\,\text{E}}
\begin{prooftree}
{
to prove={(\exists x)((\forall y)(Py \lif x = y) \land Px) \sststile{}{} (\exists x)(\forall y)(Py \liff x = y)}
}
[{(\exists x)((\forall y)(Py \lif x = y) \land Px)}, checked=a, just=Pr., name=pr
[{\lnot (\exists x)(\forall y)(Py \liff x = y)}, subs=a, just=Conc.~neg., name=neg conc
[{(\forall y)(Py \lif a = y) \land Pa}, checked, just=$\exists\elim$:pr
[{(\forall y)(Py \lif a = y)}, subs=b, just=$\land\elim$:!u, name=mark
[Pa, just=$\land\elim$:!uu, name=simple
[{\lnot (\forall y)(Py \liff a = y)}, checked=b, just=$\lnot\exists\elim$:neg conc
[{\lnot (Pb \liff a = b)}, checked, just=$\lnot\forall\elim$:!u
[Pb, just=$\liff\elim$:!u, name=to Pb or not to Pb
[a \neq b, just=$\liff\elim$:!u
[{Pb \lif a = b}, checked, just=$\forall\elim$:mark, move by=1
[\lnot Pb, close={:to Pb or not to Pb,!c}, just=$\lif\elim$:!u
]
[{a = b}
[a \neq a, close={:!c}, just={$=\elim$:{!uuu,!u}}
]
]
]
]
]
[\lnot Pb
[{a = b}
[Pb, just={$=\elim$:{simple,!u}}, close={:to Pb or not to Pb,!c}
]
]
]
]
]
]
]
]
]
]
\end{prooftree}
\end{document}
