1 \documentclass{article}

     2 \usepackage{charter}

     3 \usepackage{proof}

     4 

     5 \begin{document}

     6 

     7 \section*{Inference Rules}

     8 

     9 \begin{enumerate}

    10 \item Frequently used inference rules:

    11 

    12 \begin{center}

    13 \mbox{\infer{F,\Gamma \vdash F}{}}\medskip

    14 

    15 \mbox{\infer{\Gamma \vdash F_2}

    16             {\Gamma \vdash F_1 \Rightarrow F_2 & \Gamma \vdash F_1}}

    17 \hspace{10mm}

    18 \mbox{\infer{\Gamma \vdash F_1 \Rightarrow F_2}

    19             {F_1, \Gamma \vdash F_2}}\medskip

    20 

    21 \mbox{\infer{\Gamma \vdash P \;\textit{says}\; F}

    22             {\Gamma \vdash F}}

    23 \hspace{10mm}

    24 \mbox{\infer[\star]{\Gamma \vdash F}

    25             {\Gamma \vdash P \;\textit{controls}\; F & \Gamma \vdash P

    26               \;\textit{says}\; F}}\medskip

    27 

    28 \mbox{\infer{\Gamma \vdash P \;\textit{says}\;F_2}

    29             {\Gamma \vdash P \;\textit{says}\; (F_1 \Rightarrow F_2) & 

    30              \Gamma \vdash P \;\textit{says}\;F_1}}\medskip

    31 

    32 \mbox{\infer{\Gamma \vdash F[x := t]}

    33             {\Gamma \vdash \forall x. F}}\medskip

    34 

    35 \mbox{\infer{\Gamma \vdash F_1 \wedge F_2}

    36             {\Gamma \vdash F_1 & \Gamma \vdash F_2}}

    37 \hspace{10mm}

    38 \mbox{\infer{\Gamma \vdash F_1}

    39             {\Gamma \vdash F_1 \wedge F_2}}

    40 \hspace{10mm}

    41 \mbox{\infer{\Gamma \vdash F_2}

    42             {\Gamma \vdash F_1 \wedge F_2}}\medskip

    43 

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

    45     \Gamma \vdash P\;\textit{says}\; F}}

    46 \end{center}

    47 

    48 \item Less frequently used inference rules:

    49 

    50 \begin{center}

    51 \mbox{\infer{\Gamma \vdash slev(P) < slev(Q)}

    52             {\Gamma \vdash slev(P) = l_1 & \Gamma \vdash slev(Q) = l_2 &

    53               \Gamma \vdash l_1 < l_2}}\medskip

    54 

    55 \mbox{\infer{\Gamma \vdash slev(P) = slev(Q)}

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

    57 

    58 \mbox{\infer{\Gamma \vdash l_1 < l_3}

    59             {\Gamma \vdash l_1 < l_2 & \Gamma \vdash l_2 < l_3}}\medskip

    60 

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

    62     \vdash Q \mapsto R}}\medskip

    63 

    64 

    65 \mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}

    66 \hspace{5mm}

    67 \mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}

    68 \hspace{5mm}

    69 \mbox{\infer{\Gamma \vdash F_3}{\Gamma \vdash F_1 \vee F_2 & F_1, \Gamma

    70     \vdash F_3 & F_2, \Gamma \vdash F_3}}\medskip

    71 

    72 \mbox{\infer[c\;\mbox{must be a fresh variable}]{\Gamma \vdash \forall

    73     x. F}{\Gamma \vdash F[x := c]}}\medskip

    74 

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

    76 

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

    78     & \Gamma \vdash Q\;\textit{controls} F}}

    79 

    80 

    81 \end{center}

    82 \end{enumerate}

    83 

    84 

    85 $\star$ derived rules

    86 \end{document}

    87 

    88 %%% Local Variables: 

    89 %%% mode: latex

    90 %%% TeX-master: t

    91 %%% End: