Typesetting horizontal line used in logic

Question

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

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.

Answer 1

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}

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}

Answer 2

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

Answer 3

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.