我喜欢垂直堆叠使用 bussproofs 构建的证明规则。为了使用标签和标签,我将证明树封闭在方程式中,这就是为什么我引入 rawprooftree 环境,正如之前在对方程式等式的连续证明进行编号。直接封闭总线防护树不起作用。
但是,生成的堆栈很难看,因为规则没有居中。如何才能实现证明树相对于彼此居中?
代码如下:
\documentclass[fontsize=11pt,paper=a4,headsepline,footsepline,DIV=13,BCOR=12mm,bibliography=toc,chapterprefix=on]{scrbook}
\usepackage[T1]{fontenc}
\usepackage[ngerman,american]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{varwidth}
\usepackage{bussproofs} % sequent-calculus-style proofs
\usepackage{caption}
\captionsetup{format=plain, width=.9\textwidth}
\usepackage{subcaption}
\newenvironment{rawprooftree}
{\varwidth{.9\linewidth}\centering\leavevmode}
{\DisplayProof\endvarwidth}
\begin{document}
\begin{figure}[h]
\centering
\begin{small}
\fbox{\begin{subfigure}[t]{.45\textwidth}%
\begin{equation*}\tag{$\forall$R}\label{rule:forallR}%
\begin{rawprooftree}%
\def\defaultHypSeparation{\hskip .02in}%
\AxiomC{$\Gamma \vdash \varphi_x^y, \Delta$}%
\UnaryInfC{$\Gamma \vdash \forall x. \varphi, \Delta$}%
\end{rawprooftree}%
\end{equation*}%
\begin{equation*}\tag{CEL}\label{rule:CEL}%
\begin{rawprooftree}%
\def\defaultHypSeparation{\hskip .02in}%
\AxiomC{$\Gamma \vdash C(Q), \Delta$}%
\AxiomC{$P \leftrightarrow Q$}%
\BinaryInfC{$\Gamma \vdash C(P), \Delta$}%
\end{rawprooftree}%
\end{equation*}%
\end{subfigure}}%
\end{small}
\end{figure}
\end{document}
答案1
问题是它0.45\textwidth
太小了。
使用0.5\textwidth
解决了这个问题(对于特定的树)。输入也可以大大简化。varwidth
实际上没有必要,至少在这个应用程序中不需要。
\documentclass[fontsize=11pt,paper=a4,headsepline,footsepline,DIV=13,BCOR=12mm,bibliography=toc,chapterprefix=on]{scrbook}
\usepackage[T1]{fontenc}
\usepackage[ngerman,american]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{bussproofs} % sequent-calculus-style proofs
\newenvironment{rawprooftree}{}{\DisplayProof}
\begin{document}
\begin{figure}[htp]
\centering\small
\fbox{\begin{minipage}{0.50\textwidth}
\vspace*{-0.5\baselineskip}
\begin{gather*}
\tag{$\forall$R}\label{rule:forallR}
\begin{rawprooftree}
\def\defaultHypSeparation{\hskip .02in}
\AxiomC{$\Gamma \vdash \varphi_x^y, \Delta$}
\UnaryInfC{$\Gamma \vdash \forall x. \varphi, \Delta$}
\end{rawprooftree}
\\
\tag{CEL}\label{rule:CEL}%
\begin{rawprooftree}
\def\defaultHypSeparation{\hskip .02in}
\AxiomC{$\Gamma \vdash C(Q), \Delta$}
\AxiomC{$P \leftrightarrow Q$}
\BinaryInfC{$\Gamma \vdash C(P), \Delta$}
\end{rawprooftree}
\end{gather*}
\vspace*{-0.5\baselineskip}
\end{minipage}}
\end{figure}
\end{document}