Inference rules: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 1: Linia 1:
 
== Inference rules of algorithmic logic ==
 
== Inference rules of algorithmic logic ==
  
<span style="color: Blue"><math>|{R_1\}\qquad\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }  </math></span>
+
<span style="color: Blue"><math>\{R_1\}\qquad\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }  </math></span>
 +
 
 
<span style="color: Blue"><math>\{R_2\}\qquad \dfrac{(\alpha \Rightarrow \beta )}{(K\alpha \Rightarrow K\beta )}  </math></span>
 
<span style="color: Blue"><math>\{R_2\}\qquad \dfrac{(\alpha \Rightarrow \beta )}{(K\alpha \Rightarrow K\beta )}  </math></span>
 +
 
<span style="color: Blue"><math>\{R_3\}\qquad  \dfrac{\{s({\bf if}\ \gamma \ {\bf then}\ K\ {\bf fi})^{i}(\lnot
 
<span style="color: Blue"><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 \wedge \alpha )\Longrightarrow \beta \}_{i\in N}}{(s({\bf while}\
 
\gamma \ {\bf do}\ K\ {\bf od}\ \alpha )\Longrightarrow \beta )}  </math></span>
 
\gamma \ {\bf do}\ K\ {\bf od}\ \alpha )\Longrightarrow \beta )}  </math></span>
 +
 
<span style="color: Blue"><math>\{R_4\}\qquad  \dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup
 
<span style="color: Blue"><math>\{R_4\}\qquad  \dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup
 
K\alpha \Longrightarrow \beta )}  </math></span>
 
K\alpha \Longrightarrow \beta )}  </math></span>
 +
 
<span style="color: Blue"><math>\{R_5\}\qquad  \dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha
 
<span style="color: Blue"><math>\{R_5\}\qquad  \dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha
 
\Longrightarrow \bigcap K\beta )}  </math></span>
 
\Longrightarrow \bigcap K\beta )}  </math></span>
 +
 
<span style="color: Blue"><math>\{R_6\}\qquad  \dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists
 
<span style="color: Blue"><math>\{R_6\}\qquad  \dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists
 
x)\alpha (x)~\Longrightarrow ~\beta )}  </math></span>
 
x)\alpha (x)~\Longrightarrow ~\beta )}  </math></span>
 +
 
<span style="color: Blue"><math>\{R_7\}\qquad  \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta
 
<span style="color: Blue"><math>\{R_7\}\qquad  \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta
 
\Longrightarrow (\forall )\alpha (x))}  </math></span>
 
\Longrightarrow (\forall )\alpha (x))}  </math></span>

Wersja z 09:59, 19 lis 2015

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