☰

ebproof 中的堆叠假设

tag-icon • tag-icon logic ebproof
ebproof 中的堆叠假设

我正在尝试使用 ebproof 包编写证明树。我有一长串谓词，其中大多数都很短，但有一个谓词很长，例如：

\begin{prooftree}
    \hypo{h_0}
    \hypo{h_1}
    \hypo{h_2}
    \hypo{h_3 : \textit{a long predicate}}
    \hypo{h_4}
    \infer5[label]{\textit{conclusion}}
\end{prooftree}

现在由于长度h_3我想堆叠假设来呈现类似的东西：

   h_0     h_1     h_2
h_3 : a long predicate  h_4 
---------------------------- Label
        conclusion

我已经想出了两个相关的解决方案，使用内部证明树来堆叠假设，但两者都有些奇怪。

第一次尝试：

\begin{figure}
\begin{center}
\begin{prooftree}
    \hypo{h_0}
    \hypo{h_1}
    \hypo{h_2}
    \infer[no rule]3{
        \begin{prooftree}
            \hypo{h_3 : \textit{a long predicate}}
            \hypo{h_4}
            \infer[simple]2[label]{\textit{conclusion}}
        \end{prooftree}
    }
\end{prooftree}
\end{center}
\end{figure}

这几乎可行，但第一行最终位于整个内部证明树的中心，包括标签，例如：

        h_0     h_1     h_2
h_3 : a long predicate  h_4 
---------------------------- Label
        conclusion

现在我可以通过使内部证明树中的推理为空并向外部树添加 infer1 来纠正此问题。这样做效果更好，但会插入一些奇怪的多余垂直空白（可能是执行空推理）：

\begin{figure}
\begin{center}
\begin{prooftree}
    \hypo{h_0}
    \hypo{h_1}
    \hypo{h_2}
    \infer[no rule]3{
        \begin{prooftree}
            \hypo{h_3 : \textit{a long predicate}}
            \hypo{h_4}
            \infer2{}
        \end{prooftree}
    }
    \infer1[label]{\textit{conclusion}}
\end{prooftree}
\end{center}
\end{figure}

结果是：

   h_0     h_1     h_2
h_3 : a long predicate  h_4 

---------------------------- Label
        conclusion

有没有更好的方法来实现这一点？如果没有，是否有一种可靠的方法来修复这两种方法？

完整工作示例：

\documentclass{article}

\usepackage{ebproof}

\begin{document}

% overfull hbox 
\begin{figure}
\begin{center}
\begin{prooftree}
    \hypo{h_0}
    \hypo{h_1}
    \hypo{h_2}
    \hypo{h_3 : \textit{a long predicate}}
    \hypo{h_4}
    \infer5[label]{\textit{conclusion}}
\end{prooftree}
\end{center}
\end{figure}

% weird alingment
\begin{figure}
\begin{center}
\begin{prooftree}
    \hypo{h_0}
    \hypo{h_1}
    \hypo{h_2}
    \infer[no rule]3{
        \begin{prooftree}
            \hypo{h_3 : \textit{a long predicate}}
            \hypo{h_4}
            \infer[simple]2[label]{\textit{conclusion}}
        \end{prooftree}
    }
\end{prooftree}
\end{center}
\end{figure}

% excess vertical space
\begin{figure}
\begin{center}
\begin{prooftree}
    \hypo{h_0}
    \hypo{h_1}
    \hypo{h_2}
    \infer[no rule]3{
        \begin{prooftree}
            \hypo{h_3 : \textit{a long predicate}}
            \hypo{h_4}
            \infer2{}
        \end{prooftree}
    }
    \infer1[label]{\textit{conclusion}}
\end{prooftree}
\end{center}
\end{figure}

\end{document}

答案1

我找到了解决方案。可以使用选项 来控制推理线周围的垂直空间rule margin。通过将其设置为 0，我可以消除第二个解决方案中的多余空白：

\begin{figure}
\begin{center}
\begin{prooftree}
    \hypo{h_0}
    \hypo{h_1}
    \hypo{h_2}
    \infer[no rule]3{
        \begin{prooftree}[rule margin=0ex]
            \hypo{h_3 : \textit{a long predicate}}
            \hypo{h_4}
            \infer2{}
        \end{prooftree}
    }
    \infer1[label]{\textit{conclusion}}
\end{prooftree}
\end{center}
\end{figure}

编辑：

对此的概括是

% Usage:
%   #1 : Number of \hypo in line 1 
%   #2 : line 1, it probably will do weird things if its not just a series of \hypo 
%   #3 : Number of \hypo in line 2
%   #4 : line 2, same note as above
\newcommand{\stackedhypos}[4]{%
    \hypo{
        \begin{prooftree}
            #2 % line 1
            \infer[no rule]#1{ 
                \begin{prooftree}[rule margin=0ex]
                    #4 % line 2
                    \infer[no rule]#3{}
                \end{prooftree}
            }
        \end{prooftree}
    }
}

\begin{figure}
\begin{center}
\begin{prooftree}
    \stackedhypos3{
        \hypo{h_0}
        \hypo{h_1}
        \hypo{h_2}
    }2{
        \hypo{h_3 : \textit{a long predicate}}
        \hypo{h_4}
    }
    \infer1[label]{\textit{conclusion}}
\end{prooftree}
\end{center}
\end{figure}

将线放在#2 % line 1a 内prooftree可以消除上线比下线长的错误。更直接的概括例如：

\newcommand{\stackedhypos}[4]{%
    #2 % line 1
    \infer[no rule]#1{ 
        \begin{prooftree}[rule margin=0ex]
            #4 % line 2
            \infer[no rule]#3{}
        \end{prooftree}
    }
}

将呈现如下效果（当线路交换时）：

  h_3 : a long predicate  h_4
     h_0     h_1     h_2 
     ------------------- Label
        conclusion

而不是像

  h_3 : a long predicate  h_4
     h_0     h_1     h_2 
  --------------------------- Label
        conclusion

相关内容