[Tex/LaTex] 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}