Tekst źródłowy strony Inference rules

There are seven basic inference rules and much more secondary rules 
== Basic inference rules of algorithmic logic ==

<span style="color: Blue"><math>\{R_1\}\qquad\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }  </math></span>

<span style="color: Blue"><math>\{R_2\}\qquad \dfrac{(\alpha \Rightarrow \beta )}{(K\alpha \Rightarrow K\beta )}  </math></span>

<span style="color: Blue"><math>\{R_3\}\qquad  \dfrac{\{s({\bf if}\ \gamma \ {\bf then}\ K\ {\bf fi})^{i}(\lnot
\gamma \wedge \alpha )\Longrightarrow \beta \}_{i\in N}}{(s({\bf while}\
\gamma \ {\bf do}\ K\ {\bf od}\ \alpha )\Longrightarrow \beta )}  </math></span>

<span style="color: Blue"><math>\{R_4\}\qquad  \dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup
K\alpha \Longrightarrow \beta )}  </math></span>

<span style="color: Blue"><math>\{R_5\}\qquad  \dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha
\Longrightarrow \bigcap K\beta )}  </math></span>

<span style="color: Blue"><math>\{R_6\}\qquad  \dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists
x)\alpha (x)~\Longrightarrow ~\beta )}  </math></span>

<span style="color: Blue"><math>\{R_7\}\qquad  \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta
\Longrightarrow (\forall )\alpha (x))}  </math></span>


In rules <math>R_6</math> and <math>R_7</math>, it is assumed that <math>x</math> is a variable which is not free in <math>
\beta </math>, i.e. <math>x \notin  FV(\beta )</math>. The rules are known as the rule for
introducing an existential quantifier into the antecedent of an implication
and the rule for introducing a universal quantifier into the successor
of an implication. The rules <math>R_4</math> and <math>R_5</math> are algorithmic counterparts of rules
<math>R_6</math> and <math>R_7</math>. They are of a different character, however, since their sets of
premises are in\-finite. The rule <math>R_3</math> for introducing a '''while''' into the
antecedent of an implication is of a similar nature. These three rules are
called <math>\omega</math>-rules.

The rule <math>R_{1}</math> is known as ''modus ponens'', or the ''cut'' rule.

In all the above schemes of axioms and inference rules, <math>\alpha </math>, <math>\beta </math>, 
<math>\delta </math> are arbitrary formulas, <math>\gamma </math> and <math>\gamma ^{\prime }</math> are
arbitrary open formulas, <math>\tau </math> is an arbitrary term, <math>s</math> is a finite
sequence of assignment instructions, and <math>K</math> and <math>M</math> are arbitrary
programs.
== Some secondary inference rules ==
Below you find a couple of auxiliary inference rules. It is not possible to discover all of them. If you find one, share it with the others.
<span style="color: Blue"><math>\{R_8\}\qquad  \dfrac{\gamma \Rightarrow \gamma^{\prime}}{ {\bf while}\
\gamma^{\prime} \ {\bf do}\ K\ {\bf od}\ \mathrm{true} \Rightarrow {\bf while}\
\gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} }  </math></span>