Inference rules: Różnice pomiędzy wersjami
(→Inference rules of algorithmic logic) |
|||
| Linia 1: | Linia 1: | ||
== Inference rules of algorithmic logic == | == Inference rules of algorithmic logic == | ||
| − | <math>\tag{ | + | <math>\tag{R_1}<span style="color: Blue">\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta } </span> </math> |
| − | + | <math>\tag{R_2}<span style="color: Blue"> \dfrac{(\alpha \Rightarrow \beta )}{(K\alpha \Rightarrow K\beta )} </span> </math> | |
| − | \ | + | <math>\tag{R_3}<span style="color: Blue"> \dfrac{\{s({\bf if}\ \gamma \ {\bf then}\ K\ {\bf fi})^{i}(\lnot |
| − | (\alpha \Rightarrow \beta )}{(K\alpha \Rightarrow K\beta ) | + | |
| − | } | + | |
| − | \ | + | |
\gamma \wedge \alpha )\Longrightarrow \beta \}_{i\in N}}{(s({\bf while}\ | \gamma \wedge \alpha )\Longrightarrow \beta \}_{i\in N}}{(s({\bf while}\ | ||
| − | \gamma \ {\bf do}\ K\ {\bf od}\ \alpha )\Longrightarrow \beta )} | + | \gamma \ {\bf do}\ K\ {\bf od}\ \alpha )\Longrightarrow \beta )} </span> </math> |
| − | \ | + | <math>\tag{R_4}<span style="color: Blue"> \dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup |
| − | K\alpha \Longrightarrow \beta )} | + | K\alpha \Longrightarrow \beta )} </span> </math> |
| − | \ | + | <math>\tag{R_5}<span style="color: Blue"> \dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha |
| − | \Longrightarrow \bigcap K\beta )} | + | \Longrightarrow \bigcap K\beta )} </span> </math> |
| − | \ | + | <math>\tag{R_6}<span style="color: Blue"> \dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists |
| − | x)\alpha (x)~\Longrightarrow ~\beta )} | + | x)\alpha (x)~\Longrightarrow ~\beta )} </span> </math> |
| − | \ | + | <math>\tag{R_7}<span style="color: Blue"> \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta |
| − | \Longrightarrow (\forall )\alpha (x))} | + | \Longrightarrow (\forall )\alpha (x))} </span> </math> |
| − | + | ||
| + | |||
In rules $R_6$ and $R_7$, it is assumed that $x$ is a variable which is not free in $ | 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 | \beta $, i.e. $x \notin FV(\beta )$. The rules are known as the rule for | ||
Wersja z 10:49, 19 lis 2015
Inference rules of algorithmic logic
[math]\tag{R_1}\ltspan style="color: Blue"\gt\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta } \lt/span\gt [/math] [math]\tag{R_2}\ltspan style="color: Blue"\gt \dfrac{(\alpha \Rightarrow \beta )}{(K\alpha \Rightarrow K\beta )} \lt/span\gt [/math] [math]\tag{R_3}\ltspan style="color: Blue"\gt \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 )} \lt/span\gt [/math] [math]\tag{R_4}\ltspan style="color: Blue"\gt \dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup K\alpha \Longrightarrow \beta )} \lt/span\gt [/math] [math]\tag{R_5}\ltspan style="color: Blue"\gt \dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha \Longrightarrow \bigcap K\beta )} \lt/span\gt [/math] [math]\tag{R_6}\ltspan style="color: Blue"\gt \dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists x)\alpha (x)~\Longrightarrow ~\beta )} \lt/span\gt [/math] [math]\tag{R_7}\ltspan style="color: Blue"\gt \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta \Longrightarrow (\forall )\alpha (x))} \lt/span\gt [/math]
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 suc\-ces\-sor
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 \textbf{while} into the
antecedent of an implicationis of a similar nature. These three rules are
called $\omega $-rules.
The rule $R_{1}$ is known as \textit{modus ponens}, or the \textit{cut} rule.
In all the above schemes of axioms and inference rules, $\alpha $, $\beta $, $\delta $ are arbi\-trary for\-mulas, $\gamma $ and $\gamma ^{\prime }$ are arbitrary open formulas, $\tau $ is an arbitrary term, $s$ is a finite se\-quence of assignment instructions, and $K$ and $M$ are arbitrary programs.
