# Inference rules

(różn.) ← poprzednia wersja | przejdź do aktualnej wersji (różn.) | następna wersja → (różn.)
Skocz do: nawigacji, wyszukiwania

There are seven basic inference rules and much more secondary rules

## Basic inference rules of algorithmic logic

$\{R_1\}\qquad\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }$

$\{R_2\}\qquad \dfrac{(\alpha \Rightarrow \beta )}{(K\alpha \Rightarrow K\beta )}$

$\{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 )}$

$\{R_4\}\qquad \dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup K\alpha \Longrightarrow \beta )}$

$\{R_5\}\qquad \dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha \Longrightarrow \bigcap K\beta )}$

$\{R_6\}\qquad \dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists x)\alpha (x)~\Longrightarrow ~\beta )}$

$\{R_7\}\qquad \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta \Longrightarrow (\forall )\alpha (x))}$

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

The rule $R_{1}$ is known as modus ponens, or the cut rule.

In all the above schemes of axioms and inference rules, $\alpha$, $\beta$, $\delta$ are arbitrary formulas, $\gamma$ and $\gamma ^{\prime }$ are arbitrary open formulas, $\tau$ is an arbitrary term, $s$ is a finite sequence of assignment instructions, and $K$ and $M$ are arbitrary programs.

## Some auxiliary (secondary) inference rules

Below you find a couple of auxiliary inference rules. It is not possible to discover all useful rules. If you find one, share it with the others.

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

$\{R_9\}\qquad \dfrac{\gamma \equiv M\gamma\, , \gamma \equiv K\,M\,\gamma } {{\bf while}\ \gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} \Rightarrow {\bf while}\ \gamma \ {\bf do}\ M;K\ {\bf od}\ \mathrm{true} }$

$\{R_{10}\}\qquad \dfrac{\gamma \equiv M\gamma\, , \gamma \equiv M\,K\,\gamma } {{\bf while}\ \gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} \Rightarrow {\bf while}\ \gamma \ {\bf do}\ K;M\ {\bf od}\ \mathrm{true} }$

$\{R_{11}\}\qquad \dfrac{\gamma \land \alpha \Rightarrow K\alpha\, ,{\bf while}\ \gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} } {{\bf while}\ \gamma \ {\bf do}\ K\ {\bf od}\ \alpha }$

Put here any sound rule you encountered in your practice of verifying programs.