有人知道如何在 bussproofs 中处理这些点（间隙）吗？

Question

我正在尝试做一些类似于图片中证明的事情，其中​​证明步骤之间存在差距。我尝试了 bussproofs-extra 包，但它不允许我将两个推理中的点聚合到一个推理中（即类似于 BinaryInf，但点从两个 UnaryInf 指向它）。任何帮助都将不胜感激！

例如，没有点的样本将如下所示：

\documentclass{article}
\usepackage{bussproofs}
\usepackage{tikz}
\usepackage{bussproofs-extra}
\usepackage{amssymb,amsmath}


\begin{document} 
\begin{prooftree}
\def\fCenter{\mbox{\ $\vdash$\ }}
\AxiomC{} 
\UnaryInf$\Gamma, \varphi \fCenter \Delta$
\AxiomC{}
\UnaryInf$\Gamma\fCenter \varphi, \Delta$\RightLabel{\scriptsize Cut}
\BinaryInf$ \Gamma \fCenter \Delta$ 
\end{prooftree}   


\end{document}  

Answer 1

我已通过 Twitter 收到答复——感谢 Shawn Standefer！具体做法如下：

    \documentclass{article}
    \usepackage{bussproofs}
    \usepackage{tikz}
    \usepackage{bussproofs-extra}
    \usepackage{amssymb,amsmath}
    
    
\begin{document}

\begin{prooftree}
        \def\fCenter{\mbox{\ $\vdash$\ }}
        \AxiomC{}\LeftLabel{\scriptsize $\square$}\RightLabel{\scriptsize $n$}
        \UnaryInfC{$\Gamma \fCenter \varphi$}
        \AxiomC{}\LeftLabel{\scriptsize $\square$}\RightLabel{\scriptsize $n$}
        \UnaryInfC{$\Delta, \varphi \fCenter \psi$}
        \noLine
        \BinaryInfC{$\ddots\ \ \ \reflectbox{$\ddots$}$}
        \noLine
        \UnaryInfC{$\vdots$}
        \noLine
        \UnaryInfC{$\Gamma, \Delta \fCenter \psi$}\RightLabel{\scriptsize Cut-Un-I, $n$}
        \UnaryInfC{$\Gamma, \Delta \fCenter Un(\ulcorner \varphi \urcorner)$}
\end{prooftree}

\end{document}

它需要 reflectbox 并将其用作二元推理。noLine 只是删除了推理的水平线。