语义包：带有嵌套 \inference 的浮动前提

Question

我正在输入使用该包semantic及其命令设置一些大步骤语义\inference。

我使用 LuaLaTeX 编译器。

然而，当我编写更多inference命令时，其中一个命令代表一个公理，即没有任何前提的规则，另一个前提开始浮动。它看起来像是在尝试进行某种垂直对齐。

以下是一个例子：

\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

在 OP 的例子中，基线在大“分子”上被保留。虽然有人可能会认为这是正确的做法，但人们可以通过\abovebaseline[-\dp\strutbox]{...}应用于 ED-Skip 推理来覆盖该默认设置。

\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}