☰

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것은 약간 해킹적이지만 \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|}}의 경우 최종 라인(깊이, 즉 기준선 아래)에 유용한 "상단 스트럿"은 무시됩니다.

전체 스트럿은 중간 라인에 유용합니다. 높이도 깊이도 무시되지 않습니다.

두 번째 디스플레이에서는 더 짧은 스트럿이 사용되지만 아이디어는 동일합니다.

관련 정보