Inference rules: Różnice pomiędzy wersjami

Aktualna wersja na dzień 04:22, 6 mar 2016

There are seven basic inference rules and much more secondary rules

Basic inference rules of algorithmic logic

[math]\{R_1\}\qquad\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta } [/math]

[math]\{R_2\}\qquad \dfrac{(\alpha \Rightarrow \beta )}{(K\alpha \Rightarrow K\beta )} [/math]

[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]

[math]\{R_4\}\qquad \dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup K\alpha \Longrightarrow \beta )} [/math]

[math]\{R_5\}\qquad \dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha \Longrightarrow \bigcap K\beta )} [/math]

[math]\{R_6\}\qquad \dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists x)\alpha (x)~\Longrightarrow ~\beta )} [/math]

[math]\{R_7\}\qquad \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta \Longrightarrow (\forall )\alpha (x))} [/math]

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 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.

[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]

[math]\{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} } [/math]

[math]\{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} } [/math]

[math]\{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 } [/math]

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