Semantisches Paket: Schwebende Prämissen mit verschachtelter \Inferenz

Question

Ich gebe die Semantik einiger großer Schritte mithilfe des Pakets semanticund seines Befehls ein \inference.

Ich verwende den LuaLaTeX-Compiler.

Wenn ich jedoch mehrere inferenceBefehle erstelle und einer davon ein Axiom darstellt, also eine Regel ohne Prämissen, beginnt die andere Prämisse zu schweben. Es sieht so aus, als würde versucht, eine vertikale Ausrichtung vorzunehmen.

Hier ist ein Beispiel:

\inference[\(\mathcal{E'}=\) \textsc{EC-IfF}]
{ 
    % ------- THIS PREMISE FLOATS
    \overset{\mathcal{E'_0}}
    {
             \langle b, σ \rangle \downarrow \texttt{false}
    }
    &
    {
        \inference
        [\textsc{EC-Skip}]
        {}
        {
        \langle \texttt{skip}, σ \rangle \downarrow σ
    }
    }
}
{
            \langle
            \texttt{if } b \texttt{ then } 
            (c_0 ; \texttt{ while } b \texttt{ do } c_0)
            \texttt{ else skip}, σ
            \rangle
    \downarrow
    σ''
}

Answer 1

Im Beispiel des OP bleibt die Grundlinie über den großen „Zähler“ hinweg erhalten. Man könnte zwar argumentieren, dass dies die richtige Vorgehensweise ist, man kann diese Vorgabe jedoch überschreiben, indem man sie \abovebaseline[-\dp\strutbox]{...}auf die ED-Skip-Inferenz anwendet.

\documentclass{article}
\usepackage{semantic,amsmath,stackengine}
\begin{document}
\inference[\(\mathcal{E'}=\) \textsc{EC-IfF}]
{ 
    % ------- THIS PREMISE FLOATS
    \overset{\mathcal{E'_0}}
    {
             \langle b, σ \rangle \downarrow \texttt{false}
    }
    &
    {
        \abovebaseline[-\dp\strutbox]{\inference
        [\textsc{EC-Skip}]
        {}
        {
        \langle \texttt{skip}, σ \rangle \downarrow σ
    }}
    }
}
{
            \langle
            \texttt{if } b \texttt{ then } 
            (c_0 ; \texttt{ while } b \texttt{ do } c_0)
            \texttt{ else skip}, σ
            \rangle
    \downarrow
    σ''
}
\end{document}