以下代码:
\documentclass[10pt,journal,a4paper]{IEEEtran}
\usepackage{proof}
\usepackage{float}
\begin{document}
\begin{figure}
\infer[\textnormal{axiom} \, C]
{ C }
{ }
\vspace{5pt}
\infer[\textnormal{assume} \, L]
{ L \lor \lnot L }
{ }
\vspace{5pt}
\infer[\textnormal{subst} \, s]
{ C[s] }
{ C }
\infer[\textnormal{resolve} \, L]
{ C \lor D }
{ L \lor C \quad \lnot L \lor D }
\vspace{5pt}
\infer[\textnormal{refl} \; t]
{ t = t }
{ }
\vspace{5pt}
\infer[\textnormal{equality} \, L \, p \, t]
{ \lnot (s = t) \lor \lnot L \lor L' }
{ }
\caption{Current rules in the Metis prover}
\label{fig:move-definition}
\end{figure}
\end{document}
产生以下输出:
如何将所有水平规则右对齐?