Inference rules: Różnice pomiędzy wersjami
| Linia 26: | Linia 26: | ||
\beta </math>, i.e. <math>x \notin FV(\beta )</math>. The rules are known as the rule for | \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 | introducing an existential quantifier into the antecedent of an implication | ||
| − | and the rule for introducing a universal quantifier into the | + | 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 | 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 | <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 | + | premises are in\-finite. The rule <math>R_3</math> for introducing a '''while''' into the |
| − | antecedent of an | + | antecedent of an implication is of a similar nature. These three rules are |
| − | called <math>\omega</math> | + | called <math>\omega</math>-rules. |
| − | The rule <math>R_{1}</math> is known as | + | 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>, | In all the above schemes of axioms and inference rules, <math>\alpha </math>, <math>\beta </math>, | ||
| − | <math>\delta </math> are | + | <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 | 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. | 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 \ {\bf do}\ K\ {\bf od}\ \mathrm{true} )\Rightarrow {\bf while}\ | ||
| + | \gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} )} </math></span> | ||
Wersja z 11:20, 19 lis 2015
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 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. [math]\{R_8\}\qquad \dfrac{\gamma \Rightarrow \gamma^{\prime}}{ {\bf while}\ \gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} )\Rightarrow {\bf while}\ \gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} )} [/math]
