排版逻辑中使用的水平线

Question

我正在尝试排版一组微积分规则，其外观应如附图中的示例所示。

示例中的规则以经典的逻辑符号书写。

我特别想知道将需求与结论分开的水平线。如何排版此行以使其自动扩展？

非常感激你的帮助。

Answer 1

这很容易bussproofs；最难的部分是获得对齐。

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

另一种解决方案，它还提供了一个boxedprooftree可以在任何地方使用的环境。它有一个用于垂直对齐的可选参数，就像或一样tabular：\parbox它可以是t或b用于顶部或底部对齐（默认c为垂直居中）。

\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

您可以使用分数：

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

导致

Answer 3

这是改编自egreg 的回答使用ebproof受到启发bussproofs并且具有相当相似的语法。

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

带星号的环境版本相当于将无星号的版本包装在center环境中。该环境可用于文本或数学模式。