☰

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環境有點hacky，但這是我可以為 中的 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|}}類似，對於底線（深度，即基線以下的部分）有用的「頂部支柱」被忽略。

完整的支柱對於中線很有用：高度和深度都不會被忽略。

在第二個顯示器中，使用了較短的支柱，但想法是相同的。

相關內容