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
    Commented Oct 28, 2021 at 20:27

1 Answer 1

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
    Commented Oct 29, 2021 at 17:46

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .