Inference rules: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(Some auxiliary (secondary) inference rules)
 
(Nie pokazano 2 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 40: Linia 40:
 
sequence of assignment instructions, and <math>K</math> and <math>M</math> are arbitrary
 
sequence of assignment instructions, and <math>K</math> and <math>M</math> are arbitrary
 
programs.
 
programs.
== Some secondary inference rules ==
+
== Some auxiliary (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.
+
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.<br />
 +
 
 
<span style="color: Blue"><math>\{R_8\}\qquad  \dfrac{\gamma \Rightarrow \gamma^{\prime}}{ {\bf while}\
 
<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^{\prime} \ {\bf do}\ K\ {\bf od}\ \mathrm{true} \Rightarrow {\bf while}\
 
\gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} }  </math></span>
 
\gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} }  </math></span>
 +
 +
<span style="color: Blue"><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></span>
 +
 +
<span style="color: Blue"><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></span>
 +
 +
<span style="color: Blue"><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></span>
 +
 +
<span style="color: Brown">Put here any sound rule you encountered in your practice of verifying programs. </span>

Aktualna wersja na dzień 03: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.