3

I like to stack proof rules build with bussproofs vertically. In order to use tags and labels I enclose the proof tress inside a equation, which is why I introduced the rawprooftree environment as suggested earlier in Numbering sequent proofs like equations. Directly enclosing bussproofs trees does not work.

However, the resulting stack is ugly, because the rules are not centered. How can I achieve that the proof trees are centered relative to each other?

enter image description here

The code is as follows:

\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
  • Welcome to the TeX.SE. community.
    – Sebastiano
    Oct 28 '21 at 20:27
3

The problem is that 0.45\textwidth is too small.

Using 0.5\textwidth solves the issue (for the particular trees). Also the input can be vastly simplified. The varwidth is actually not necessary, at least in this application.

\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}

enter image description here

1
  • Thank you very very much to have read my comment in chat.
    – Sebastiano
    Oct 29 '21 at 17:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.