如何获取包含伪代码的证明规则？

Question

我希望使用包将一些霍尔逻辑的推理规则排版为伪代码序列algorithmic。我尝试使用\frac{}{}，但结果 egif then else被压平了。我也尝试过bussproofs。伪代码再次被压平为一行。

有什么好办法可以实现（当然要用更短的 hline）

{ 我 ∧ B } S { 我 }

---

{ 我 }

while B do
  S
od

{ 我 ∧ ¬ B }

我到目前为止的努力所看到的结果类似于

{ 我 ∧ B } S { 我 }

---

{ I } while B do Sod { I ∧ ¬ B }

现在，我正在尝试将底部的 Hoare-triple 放入小页面中。

\documentclass{beamer}
\usepackage{algorithmic}
\usepackage{bussproofs}

\renewcommand{\algorithmicendwhile}{{\bf od}}
\newcommand{\textmath}[1]{\text{\it #1}}

\newenvironment{Condition}{\{\,}{\,\}\;}
\newenvironment{Pseudocode}{\begin{algorithmic}}{\end{algorithmic}}
\newcommand{\hoareTripleMM}[3]{\{\,#1\,\}\;#2\;\{\,#3\,\}}

\begin{document}

\begin{frame}
  \begin{prooftree}
    \AxiomC{\(\hoareTripleMM{V}{\textmath{init}}{I}\)}
    \AxiomC{\(\hoareTripleMM{I \land B}{S}{I}\)}
    \AxiomC{\((I \land \neg B) \implies P\)}
    \RightLabel{(W2)}
    \TrinaryInfC{
      \begin{minipage}{68pt}
        \(
        \begin{Condition}
          V
        \end{Condition}\)
        \begin{Pseudocode}
          \STATE \(\textmath{init}\) 
          \WHILE{\(B\)} \(S\) \ENDWHILE
        \end{Pseudocode}
        \(
        \begin{Condition}
          P
        \end{Condition}\)
      \end{minipage}
    }
  \end{prooftree}
\end{frame}
\end{document}

仍然存在一些问题：

1. 前提条件和伪代码之间存在垂直空间，我还不知道它来自哪里。
2. 出现一个 LaTeX 错误：“出现问题 - 可能缺少 \item。”只有当时钟Pseudocode在其中时才会发生。
3. 我希望的宽度minipage取自伪代码的宽度。

如果可能的话我想使用它algorithmic，因为我已经经常使用这个包了。

Answer 1

环境algorithmic只是一个list，因此它会排版为当前行宽。因此无法避免指定 的宽度minipage。

为了避免占用太大空间，只需\endgraf在第一个元素后添加：

\documentclass{article}
\usepackage{algorithmic}
\usepackage{bussproofs}
\usepackage{amsmath}
\usepackage{varwidth}

\renewcommand{\algorithmicendwhile}{{\bf od}}
\newcommand{\textmath}[1]{\text{\it #1}}

\newenvironment{Condition}{\{\,}{\,\}\;}
\newenvironment{Pseudocode}{\algorithmic}{\endalgorithmic}
\newcommand{\hoareTripleMM}[3]{\{\,#1\,\}\;#2\;\{\,#3\,\}}

\begin{document}

  \begin{prooftree}
    \AxiomC{\(\hoareTripleMM{V}{\textmath{init}}{I}\)}
    \AxiomC{\(\hoareTripleMM{I \land B}{S}{I}\)}
    \AxiomC{\((I \land \neg B) \implies P\)}
    \RightLabel{(W2)}
    \TrinaryInfC{%
      \begin{minipage}{68pt}
        \(
        \begin{Condition}
          V
        \end{Condition}\)\endgraf
        \begin{Pseudocode}
          \STATE \(\textmath{init}\) 
          \WHILE{\(B\)} \STATE \(S\) \ENDWHILE
        \end{Pseudocode}
        \(
        \begin{Condition}
          P
        \end{Condition}\)
      \end{minipage}%
    }
  \end{prooftree}
\end{document}

必须使用，\endgraf因为当宏在其参数中\TrinaryInfC时它会阻塞。\par