Anpassen von Beweisregeln

Anpassen von Beweisregeln

Der folgende Code:

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

erzeugt die folgende Ausgabe:

Bildbeschreibung hier eingeben

Wie kann ich alle horizontalen Linien rechtsbündig ausrichten?

verwandte Informationen