Estou usando o ebproofpacote para criar árvores de derivação para regras de inferência. Estas regras têm premissas acima do julgamento e condições secundárias à esquerda:
Para gerar isso, eu uso:
\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*}
No entanto, estou tendo um problema em que as condições laterais se sobrepõem aos elementos circundantes. Onde há uma única inferência, posso simplesmente colocar \vspace{...}antes e depois da árvore de prova, mas onde há outra inferência (ou seja, como parte de uma árvore maior), isso não funciona ( \vspace{...}é ignorado dentro do ambiente da árvore de prova).
(Código para gerar isso:)
\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}
Existe uma maneira limpa de fazer com que ele tenha a quantidade correta de espaço? Usar o arrayambiente é um pouco complicado, mas foi a única maneira de adicionar quebras de linha ao parâmetro do rótulo esquerdo em \infer. Como alternativa, existem outros pacotes que fornecem essa sintaxe de maneira mais limpa?
Isso não é relevante para o problema, mas se você quiser copiar exatamente esses trechos de código em seu próprio documento, aqui está a definição de \triple:\newcommand{\triple}[3]{ \{#1\}\ \texttt{#2}\ \{#3\}}
Responder1
Vejo duas possibilidades.
\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}
Os espaços adicionais são obtidos com um hack, na verdade.
Com \smash[t]{\vphantom{\bigg|}}insiro a parte inferior de a \bigg|(sem imprimir o símbolo), pois \smash[t]{...}tem o cuidado de desconsiderar a altura do símbolo. Isso é útil para a linha superior, então eu chamo de “suporte inferior”.
Da mesma forma com `\smash[b]{\vphantom{\bigg|}}, um “suporte superior” útil para a linha inferior (a profundidade, ou seja, o que está abaixo da linha de base) é desconsiderado.
A escora completa é útil para a linha média: nem a altura nem a profundidade são desconsideradas.
No segundo display é utilizado um suporte mais curto, mas a ideia é a mesma.