☰

ebproof 证明树：边条件重叠

tag-icon • tag-icon white-space overlap ebproof
ebproof 证明树：边条件重叠

我正在使用该ebproof包来制作推理规则的派生树。这些规则在判断上方有前提，在左侧有附加条件：

提供证明的示例

为了生成这个，我使用：

   \begin{prooftree*}
        \hypo{\Gamma \vdash \triple{P'}{S}{Q'}}
        \infer[left label=
            $\begin{array}{r}
            Q' \geq 0 \\
            P \geq P' \\
            Q \leq Q'
            \end{array}$]
            1[\textsc{(While)}]
            { \Gamma \vdash  \triple{P}{while $e$ do $S$}{Q} }
    \end{prooftree*}

但是，我遇到了一个问题，即边条件与周围元素重叠。如果只有一个推理，我可以将其放在\vspace{...}证明树之前和之后，但是如果存在另一个推理（即作为更大树的一部分），则此方法不起作用（\vspace{...}在证明树环境中被忽略）。

堆叠推理中的重叠边条件

（生成此代码：）

    \begin{prooftree}
        \hypo{\Gamma \vdash \triple{P}{$S_1$}{Q_1}}
        \hypo{\Gamma \vdash \triple{P}{$S_2$}{Q_2}}
        \infer[left label={
            $\begin{array}{r}
            Q' \leq Q_1 \\
            Q' \leq Q_2
            \end{array}$}]
            2[\textsc{(B-Cond)}]
            { \Gamma \vdash  \triple{P}{if $e$ then $S_1$ else $S_2$}{Q} }
        \infer
        [left label={$
        \begin{array}{r}
            P \geq Q' \\
            Q \leq Q'
        \end{array}
        $}]
        1[\textsc{(B-Conseq)}]
        {\Gamma \vdash \triple{P}{if $e$ then $S_1$ else $S_2$}{Q}}
    \end{prooftree}

有没有一种干净的方法可以让它具有正确的空间量？使用环境array有点不方便，但这是我可以在 中的 left-label 参数中添加换行符的唯一方法\infer。或者，是否有其他软件包可以以更干净的方式提供此语法？

这与问题无关，但如果您想将这些代码片段准确地复制到您自己的文档中，这里是 \triple 的定义：\newcommand{\triple}[3]{ \{#1\}\ \texttt{#2}\ \{#3\}}

答案1

我看到两种可能性。

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

\newcommand{\triple}[3]{\{#1\}\ \texttt{#2}\ \{#3\}}
\newcommand{\bstrutb}{\smash[t]{\vphantom{\bigg|}}}
\newcommand{\bstrutt}{\smash[b]{\vphantom{\bigg|}}}
\newcommand{\bstrut}{\vphantom{\bigg|}}

\begin{document}

\section{Spacing the lines}

\begin{prooftree}
    \hypo{\bstrutb \Gamma \vdash \triple{P}{$S_1$}{Q_1}}
    \hypo{\Gamma \vdash \triple{P}{$S_2$}{Q_2}}
    \infer[left label={
        $\begin{array}{@{}r@{}}
        Q' \leq Q_1 \\
        Q' \leq Q_2
        \end{array}$}]
        2[\textsc{(B-Cond)}]
        {\bstrut \Gamma \vdash  \triple{P}{if $e$ then $S_1$ else $S_2$}{Q} }
    \infer
    [left label={
        $\begin{array}{@{}r@{}}
        P \geq Q' \\
        Q \leq Q'
        \end{array}$}]
    1[\textsc{(B-Conseq)}]
    {\bstrutt \Gamma \vdash \triple{P}{if $e$ then $S_1$ else $S_2$}{Q}}
\end{prooftree}

\section{Reducing the size, with some more space}

\begin{prooftree}
    \hypo{\Gamma \vdash \triple{P}{$S_1$}{Q_1}}
    \hypo{\Gamma \vdash \triple{P}{$S_2$}{Q_2}}
    \infer[left label={
        $\substack{
        Q' \leq Q_1 \\
        Q' \leq Q_2
        }$}]
        2[\textsc{(B-Cond)}]
        {\vphantom{\Big|}\Gamma \vdash  \triple{P}{if $e$ then $S_1$ else $S_2$}{Q} }
    \infer
    [left label={
        $\substack{
        P \geq Q' \\
        Q \leq Q'
        }$}]
    1[\textsc{(B-Conseq)}]
    {\Gamma \vdash \triple{P}{if $e$ then $S_1$ else $S_2$}{Q}}
\end{prooftree}

\end{document}

在此处输入图片描述

实际上，额外的空间是通过黑客手段获得的。

我\smash[t]{\vphantom{\bigg|}}插入了 a 的下半部分\bigg|（不打印符号），因为\smash[t]{...}忽略了符号的高度。这对于顶线很有用，所以我称之为“底部支柱”。

类似地，对于 `\smash[b]{\vphantom{\bigg|}} 来说，对底线（深度，即基线以下的部分）有用的“顶部支柱”被忽略。

充分支撑对于中线很有用：高度和深度都不容忽视。

在第二个展示中，使用了较短的支柱，但想法是一样的。

相关内容