![ebproof 中的堆叠假设](https://linux22.com/image/467039/ebproof%20%E4%B8%AD%E7%9A%84%E5%A0%86%E5%8F%A0%E5%81%87%E8%AE%BE.png)
我正在尝试使用 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 1
a 内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