![如何在 prooftrees 环境中增加证明线之间的垂直距离?](https://linux22.com/image/440915/%E5%A6%82%E4%BD%95%E5%9C%A8%20prooftrees%20%E7%8E%AF%E5%A2%83%E4%B8%AD%E5%A2%9E%E5%8A%A0%E8%AF%81%E6%98%8E%E7%BA%BF%E4%B9%8B%E9%97%B4%E7%9A%84%E5%9E%82%E7%9B%B4%E8%B7%9D%E7%A6%BB%EF%BC%9F.png)
使用以下代码,我尝试使用 prooftrees 环境创建证明树,该环境基于基于 pgf/TikZ 包的森林包:
\usepackage{pstricks}
%\usepackage{ot-tableau}
%\usepackage{ytableau}
\usepackage{forest}
\usepackage[tableaux]{prooftrees}
\usepackage{prooftrees}
\usetikzlibrary{fit}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\begin{document}
%\maketitle
\begin{tableau}
{
line no sep = 1.5cm,
just sep = 1.5cm, % Set separation of justification
for tree = { s sep'=10mm},
% close with = \absurd
}
[\sim A \supset B, just={P1}
[\sim A, just={P2}
[\sim B, draw, circle, just={$\sim$K}
[\neg(Q \lif R), just={From (2)}
[Q, just={From (4)}
[\neg R, s sep=30mm, just={From (4)} %Note "s sep" to
%spread fork below
[\neg(P \land Q), just={Alternatives from (1)}
[\neg P, close, just={Alternatives from (7)}
]
[\neg Q, close
]
]
[R, close]
]
]
]
]
]
]
\end{tableau}
\end{document}
现在我的问题是,我试图圈出一个基本的 wff(代码行 21),但是绘制的圆圈与前后的证明线重叠,正如您在输出中所看到的:
我想找到的解决方案是增加校样线之间的垂直距离。唯一的问题是我不知道如何最好地做到这一点。
也许还有其他方法可以解决整个重叠问题。这些解决方案也会受到欢迎。
非常感谢你的帮助
尼兹吉
答案1
这是一个粗略的版本,可以避免最坏的结果。我认为确实需要一个更好的解决方案prooftrees
。但是,由于我不知道这会有多困难或何时会发生,也许这对某些人会有所帮助。
\documentclass{standalone}
\usepackage[tableaux]{prooftrees}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\begin{document}
\begin{tableau}
{
line no sep = 1.5cm,
just sep = 1.5cm, % Set separation of justification
for tree = { s sep'=10mm},
% close with = \absurd
% before drawing tree={for tree={if grouped={red,typeset node}{blue,typeset node}}},
% proof tree dadfygio,
}
[\sim A \supset B, just={P1}
[\sim A, just={P2}
[\sim B, draw, circle, just={$\sim$K}, before typesetting nodes={not grouped, no edge}, outer sep=-5mm
[\neg(Q \lif R), just={From (2)}, before typesetting nodes={not grouped, no edge}
[Q, just={From (4)}
[\neg R, s sep=30mm, just={From (4)} %Note "s sep" to
%spread fork below
[\neg(P \land Q), just={Alternatives from (1)}
[\neg P, close, just={Alternatives from (7)}
]
[\neg Q, close
]
]
[R, close]
]
]
]
]
]
]
\end{tableau}
\end{document}
这不会给出下面的输出,因为 CTAN 上的当前版本会导致错误放置的闭包符号,而我之前不知何故错过了。我刚刚在代码中修复了这个问题,所以,如果我不能很快想出一个解决放大问题的好办法,我会上传一个临时更新来修复闭包符号,至少。