3

I am trying to typeset a set of rules of a calculs which should look as the examples in the attached pictured.

enter image description here

In the example rules are written in classical notation of logic.

I especially wonder about the horizontal line that splits the requirements from the conclusion. What's the best way to typeset this line such that it expands automatically?

Your help is very much appreciated.

3 Answers 3

6

It's quite easy with bussproofs; the hardest part is getting the alignment.

\documentclass{article}
\usepackage{amsmath}
\usepackage{array}
\usepackage{bussproofs}

\begin{document}

\[
\begin{tabular}{@{} l >{\centering\arraybackslash}m{.7\textwidth} @{}}
\textsc{Scope} &
  \begin{prooftree}
  \AxiomC{$A \xrightarrow{\alpha} A'$}
  \AxiomC{$u$ does not occur in $\alpha$}
  \BinaryInfC{$\nu u.A \xrightarrow{\alpha} \nu u.A'$}
  \end{prooftree}
\\
\textsc{Par} &
  \begin{prooftree}
  \AxiomC{$A \xrightarrow{\alpha} A'$}
  \AxiomC{$\mathit{bv}(\alpha)\cap\mathit{fv}(B)=\mathit{bn}(\alpha)\cap\mathit{fn}(B)=\emptyset$}
  \BinaryInfC{$A\mid B \xrightarrow{\alpha} A'\mid B$}
  \end{prooftree}
\end{tabular}
\]

\end{document}

enter image description here

A different solution, which also provides a boxedprooftree environment that can be used anywhere. It has an optional argument for vertical alignment, just like tabular or \parbox: it can be t or b for top or bottom alignment (default c for vertical centering).

\documentclass{article}
\usepackage{amsmath}
\usepackage{bussproofs}

\newenvironment{boxedprooftree}[1][c]
 {\begin{tabular}[#1]{@{}c@{}}}
 {\DisplayProof\end{tabular}}

\begin{document}

\[
\begin{tabular}{@{} l c @{}}
\textsc{Scope} &
  \begin{boxedprooftree}
  \AxiomC{$A \xrightarrow{\alpha} A'$}
  \AxiomC{$u$ does not occur in $\alpha$}
  \BinaryInfC{$\nu u.A \xrightarrow{\alpha} \nu u.A'$}
  \end{boxedprooftree}
\\[3ex]
\textsc{Par} &
  \begin{boxedprooftree}
  \AxiomC{$A \xrightarrow{\alpha} A'$}
  \AxiomC{$\mathit{bv}(\alpha)\cap\mathit{fv}(B)=\mathit{bn}(\alpha)\cap\mathit{fn}(B)=\emptyset$}
  \BinaryInfC{$A\mid B \xrightarrow{\alpha} A'\mid B$}
  \end{boxedprooftree}
\end{tabular}
\]

\end{document}

enter image description here

3
  • Thank you very much for this great answer. If you got any time to spare, I'd be happy for a little explanation of the column description of the tabular environement, i.e. @{} l >{\centering\arraybackslash}m{.7\textwidth} @{}
    – foobar
    Jan 12, 2016 at 13:10
  • The prooftree environment doesn't like to be set in a horizontal box (I believe there is a variant for this); so I resorted to put them in a minipage, which is what the m option does, with vertical centering. I'll look for an easier method.
    – egreg
    Jan 12, 2016 at 13:13
  • I just noticed when adding additional rules to the tabular the a part of them does not seem to be centered correctly.
    – foobar
    Jan 12, 2016 at 13:18
3

You can use a fraction:

\frac{A \overset{\alpha}{\to} A' \text{\hspace{1cm}\textit{u} does not occur in }\alpha}{\nu u.A \overset{\alpha}{\to} \nu u.A'}

resulting in

enter image description here

2

This is an adaption of egreg's answer using ebproof which was inspired by bussproofs and has a fairly similar syntax.

\documentclass{article}
\usepackage{amsmath}
\usepackage{ebproof}

\begin{document}

  \begin{prooftree*}
    \Hypo{A \xrightarrow{\alpha} A'}
    \Hypo{u \text{ does not occur in } \alpha}
    \Infer[left label={\textsc{Scope}}]2{\nu u.A \xrightarrow{\alpha} \nu u.A'}
  \end{prooftree*}
  \begin{prooftree*}
    \Hypo{A \xrightarrow{\alpha} A'}
    \Hypo{\mathit{bv}(\alpha)\cap\mathit{fv}(B)=\mathit{bn}(\alpha)\cap\mathit{fn}(B)=\emptyset}
    \Infer[left label={\textsc{Par}}]2{A\mid B \xrightarrow{\alpha} A'\mid B}
  \end{prooftree*}

\end{document}

The starred version of the environment is equivalent to wrapping the non-starred version in the center environment. The environment may be used in text or maths mode.

ebproof demo

You must log in to answer this question.

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