\documentclass{article}
\usepackage{charter}
\usepackage{proof}

\begin{document}

\section*{Inference Rules}

\begin{enumerate}
\item Frequently used inference rules:

\begin{center}
\mbox{\infer{F,\Gamma \vdash F}{}}\medskip

\mbox{\infer{\Gamma \vdash F_2}
            {\Gamma \vdash F_1 \Rightarrow F_2 & \Gamma \vdash F_1}}
\hspace{10mm}
\mbox{\infer{\Gamma \vdash F_1 \Rightarrow F_2}
            {F_1, \Gamma \vdash F_2}}\medskip

\mbox{\infer{\Gamma \vdash P \;\textit{says}\; F}
            {\Gamma \vdash F}}
\hspace{10mm}
\mbox{\infer[\star]{\Gamma \vdash F}
            {\Gamma \vdash P \;\textit{controls}\; F & \Gamma \vdash P
              \;\textit{says}\; F}}\medskip

\mbox{\infer{\Gamma \vdash P \;\textit{says}\;F_2}
            {\Gamma \vdash P \;\textit{says}\; (F_1 \Rightarrow F_2) & 
             \Gamma \vdash P \;\textit{says}\;F_1}}\medskip

\mbox{\infer{\Gamma \vdash F[x := t]}
            {\Gamma \vdash \forall x. F}}\medskip

\mbox{\infer{\Gamma \vdash F_1 \wedge F_2}
            {\Gamma \vdash F_1 & \Gamma \vdash F_2}}
\hspace{10mm}
\mbox{\infer{\Gamma \vdash F_1}
            {\Gamma \vdash F_1 \wedge F_2}}
\hspace{10mm}
\mbox{\infer{\Gamma \vdash F_2}
            {\Gamma \vdash F_1 \wedge F_2}}\medskip

\mbox{\infer[\star]{\Gamma \vdash Q\;\textit{says}\; F}{\Gamma \vdash P\mapsto Q &
    \Gamma \vdash P\;\textit{says}\; F}}
\end{center}

\item Less frequently used inference rules:

\begin{center}
\mbox{\infer{\Gamma \vdash slev(P) < slev(Q)}
            {\Gamma \vdash slev(P) = l_1 & \Gamma \vdash slev(Q) = l_2 &
              \Gamma \vdash l_1 < l_2}}\medskip

\mbox{\infer{\Gamma \vdash slev(P) = slev(Q)}
            {\Gamma \vdash slev(P) = l & \Gamma \vdash slev(Q) = l}}\medskip

\mbox{\infer{\Gamma \vdash l_1 < l_3}
            {\Gamma \vdash l_1 < l_2 & \Gamma \vdash l_2 < l_3}}\medskip

\mbox{\infer[\star]{\Gamma \vdash P \mapsto R}{\Gamma \vdash P\mapsto Q & \Gamma
    \vdash Q \mapsto R}}\medskip


\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}
\hspace{5mm}
\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}
\hspace{5mm}
\mbox{\infer{\Gamma \vdash F_3}{\Gamma \vdash F_1 \vee F_2 & F_1, \Gamma
    \vdash F_3 & F_2, \Gamma \vdash F_3}}\medskip

\mbox{\infer[c\;\mbox{must be a fresh variable}]{\Gamma \vdash \forall
    x. F}{\Gamma \vdash F[x := c]}}\medskip

\mbox{\infer{\Gamma \vdash \textit{true}}{}}\medskip

\mbox{\infer[\star]{\Gamma \vdash P\;\textit{controls}\; F}{\Gamma \vdash P\mapsto Q
    & \Gamma \vdash Q\;\textit{controls} F}}


\end{center}
\end{enumerate}


$\star$ derived rules
\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: