Ich verwende das ebproofPaket, um Ableitungsbäume für Inferenzregeln zu erstellen. Diese Regeln haben Prämissen über dem Urteil und Nebenbedingungen auf der linken Seite:
Um dies zu generieren, verwende ich:
\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*}
Ich habe jedoch ein Problem, bei dem sich die Nebenbedingungen mit den umgebenden Elementen überschneiden. Wo es eine einzelne Schlussfolgerung gibt, kann ich einfach \vspace{...}vor und nach dem Prooftree einfügen, aber wo es eine andere Schlussfolgerung gibt (d. h. als Teil eines größeren Baums), funktioniert dies nicht ( \vspace{...}wird innerhalb der Prooftree-Umgebung ignoriert).
(Code zum Generieren:)
\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}
Gibt es eine saubere Möglichkeit, dafür zu sorgen, dass die richtige Menge an Platz vorhanden ist? Die Verwendung der arrayUmgebung ist ein bisschen umständlich, aber es war die einzige Möglichkeit, dem linken Label-Parameter in Zeilenumbrüche hinzuzufügen \infer. Gibt es alternativ andere Pakete, die diese Syntax auf sauberere Weise bereitstellen?
Dies ist für das Problem nicht relevant, aber wenn Sie diese Codeausschnitte exakt in Ihr eigenes Dokument kopieren möchten, finden Sie hier die Definition von \triple:\newcommand{\triple}[3]{ \{#1\}\ \texttt{#2}\ \{#3\}}
Antwort1
Ich sehe zwei Möglichkeiten.
\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}
Die zusätzlichen Plätze werden eigentlich durch einen Hack erlangt.
Mit \smash[t]{\vphantom{\bigg|}}füge ich den unteren Teil von a ein \bigg|(ohne das Symbol zu drucken), weil \smash[t]{...}die Höhe des Symbols ignoriert wird. Dies ist für die obere Zeile nützlich, daher nenne ich es „untere Strebe“.
Ähnlich verhält es sich mit `\smash[b]{\vphantom{\bigg|}}: Eine „obere Strebe“, die für die untere Linie (die Tiefe, d. h. das, was sich unterhalb der Grundlinie befindet) nützlich ist, wird nicht berücksichtigt.
Für die Mittellinie ist die volle Strebe von Nutzen: weder Höhe noch Tiefe werden dabei außer Acht gelassen.
In der zweiten Darstellung wird eine kürzere Strebe verwendet, aber die Idee ist dieselbe.