如何在 prooftrees 环境中增加证明线之间的垂直距离？

Question

使用以下代码，我尝试使用 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），但是绘制的圆圈与前后的证明线重叠，正如您在输出中所看到的：

我想找到的解决方案是增加校样线之间的垂直距离。唯一的问题是我不知道如何最好地做到这一点。

也许还有其他方法可以解决整个重叠问题。这些解决方案也会受到欢迎。

非常感谢你的帮助

尼兹吉

Answer 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 上的当前版本会导致错误放置的闭包符号，而我之前不知何故错过了。我刚刚在代码中修复了这个问题，所以，如果我不能很快想出一个解决放大问题的好办法，我会上传一个临时更新来修复闭包符号，至少。