Levezetési szabályok

\[ \begin{array}{cc} 1.& Q \supset lf\big(S_0,\;Q'\big) \\\\ 2.& Q' \supset lf\big(S_1,\;R\big)\end{array} \]

\[ \begin{array}{cl} 1.& Q \supset \underset{i=1}{\overset{n}{\huge{\lor}}}\pi_i \\\\ 2.& Q\supset\underset{i=1}{\overset{n}{\huge{\land}}}\big(\pi_i\;\lor\neg\pi_i\big) \\\\ 3.& \forall i\in[1..n]:\;\big(Q\land\pi_i\big)\supset R\end{array} \]

\[ \begin{array}{cl} 1.& Q \supset P \\ 2.& (P \land \neg\pi)\supset R \\ 3.& P \supset (\pi\,\lor\neg\pi) \\ 4.& (P\land \pi) \supset (t>0) \\ 5.& (P\land \pi \land t=t_0)\supset lf(S_0,\; P\land t<t_0)\end{array} \]