Inference rules - Historia wersji

AndrzejSalwicki: /* Some auxiliary (secondary) inference rules */

2016-03-06T02:22:43Z

‎Some auxiliary (secondary) inference rules

AndrzejSalwicki: /* Some secondary inference rules */

2015-11-19T09:56:00Z

‎Some secondary inference rules

AndrzejSalwicki: /* Some secondary inference rules */

2015-11-19T09:42:24Z

‎Some secondary inference rules

AndrzejSalwicki o 09:22, 19 lis 2015

2015-11-19T09:22:54Z

AndrzejSalwicki o 09:20, 19 lis 2015

2015-11-19T09:20:48Z

AndrzejSalwicki o 09:08, 19 lis 2015

2015-11-19T09:08:44Z

AndrzejSalwicki o 08:59, 19 lis 2015

2015-11-19T08:59:39Z

AndrzejSalwicki o 08:58, 19 lis 2015

2015-11-19T08:58:21Z

AndrzejSalwicki o 08:52, 19 lis 2015

2015-11-19T08:52:37Z

AndrzejSalwicki: /* Inference rules of algorithmic logic */

2015-11-19T08:49:51Z

‎Inference rules of algorithmic logic

@@ Linia 41: / Linia 41: @@
 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.
+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}\
 \gamma^{\prime} \ {\bf do}\ K\ {\bf od}\ \mathrm{true} \Rightarrow {\bf while}\

@@ Linia 40: / Linia 40: @@
 sequence of assignment instructions, and <math>K</math> and <math>M</math> are arbitrary
 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.
 <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}\
@@ Linia 49: / Linia 49: @@
 {{\bf while}\ \gamma \ {\bf do}\ K\ {\bf od}\ \mathrm{true} \Rightarrow {\bf while}\
 \gamma \ {\bf do}\ M;K\ {\bf od}\ \mathrm{true}  }  </math></span>

← poprzednia wersja		Wersja z 09:42, 19 lis 2015
Linia 45:		Linia 45:
	\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>

@@ Linia 41: / Linia 41: @@
 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.
+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^{\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>

@@ Linia 26: / Linia 26: @@
 \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 suc\-ces\-sor
+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 \textbf{while} into the
+premises are in\-finite. The rule <math>R_3</math> for introducing a '''while''' into the
-antecedent of an implicationis of a similar nature. These three rules are
+antecedent of an implication is of a similar nature. These three rules are
-called <math>\omega</math>$-rules.
+called <math>\omega</math>-rules.
-The rule <math>R_{1}</math> is known as \textit{modus ponens}, or the \textit{cut} rule.
+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 arbi\-trary for\-mulas, <math>\gamma </math> and <math>\gamma ^{\prime }</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
-se\-quence 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.

@@ Linia 1: / Linia 1: @@
-== Inference rules of algorithmic logic ==
+There are seven basic inference rules and much more secondary rules
 <span style="color: Blue"><math>\{R_1\}\qquad\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }  </math></span>
@@ Linia 22: / Linia 23: @@
-In rules $R_6$ and $R_7$, it is assumed that $x$ is a variable which is not free in $
+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 $, i.e. $x \notin  FV(\beta )$. 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
 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
+of an implication. The rules <math>R_4</math> and <math>R_5</math> are algorithmic counterparts of rules
-$R_6$ and $R_7$. 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 $R_3$ for introducing a \textbf{while} into the
+premises are in\-finite. The rule <math>R_3</math> for introducing a \textbf{while} into the
 antecedent of an implicationis of a similar nature. These three rules are
-called $\omega $-rules.
+called <math>\omega</math>$-rules.
-The rule $R_{1}$ is known as \textit{modus ponens}, or the \textit{cut} rule.
+The rule <math>R_{1}</math> is known as \textit{modus ponens}, or the \textit{cut} rule.
-In all the above schemes of axioms and inference rules, $\alpha $, $\beta $,
+In all the above schemes of axioms and inference rules, <math>\alpha </math>, <math>\beta </math>,
-$\delta $ are arbi\-trary for\-mulas, $\gamma $ and $\gamma ^{\prime }$ are
+<math>\delta </math> are arbi\-trary for\-mulas, <math>\gamma </math> and <math>\gamma ^{\prime }</math> are
-arbitrary open formulas, $\tau $ is an arbitrary term, $s$ is a finite
+arbitrary open formulas, <math>\tau </math> is an arbitrary term, <math>s</math> is a finite
-se\-quence of assignment instructions, and $K$ and $M$ are arbitrary
+se\-quence of assignment instructions, and <math>K</math> and <math>M</math> are arbitrary
 programs.

@@ Linia 1: / Linia 1: @@
 == 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_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></span>
 <span style="color: Blue"><math>\{R_4\}\qquad  \dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup
 K\alpha \Longrightarrow \beta )}  </math></span>
 <span style="color: Blue"><math>\{R_5\}\qquad  \dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha
 \Longrightarrow \bigcap K\beta )}  </math></span>
 <span style="color: Blue"><math>\{R_6\}\qquad  \dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists
 x)\alpha (x)~\Longrightarrow ~\beta )}  </math></span>
 <span style="color: Blue"><math>\{R_7\}\qquad  \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta
 \Longrightarrow (\forall )\alpha (x))}  </math></span>

@@ Linia 1: / Linia 1: @@
 == Inference rules of algorithmic logic ==
-<math>\tag{R_1}<span style="color: Blue">\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta } </span> </math>
+<span style="color: Blue"><math>\tag{R_1}\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }  </math></span>
 <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

@@ Linia 1: / Linia 1: @@
 == Inference rules of algorithmic logic ==
-<math>\tag{R1}\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }  </math>
+<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>
-\item[$R_{2}$]\qquad $\dfrac{
+<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 )
-}$
-\item[$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 )}$
+\gamma \ {\bf do}\ K\ {\bf od}\ \alpha )\Longrightarrow \beta )} </span> </math>
-\item[$R_{4}$]\qquad  $\dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup
+<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>
-\item[$R_{5}$]\qquad $\dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha
+<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>
-\item[$R_{6}$]\qquad $\dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists
+<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>
-\item[$R_{7}$]\qquad $\dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta
+<math>\tag{R_7}<span style="color: Blue"> \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta
-\Longrightarrow (\forall )\alpha (x))}$
+\Longrightarrow (\forall )\alpha (x))} </span> </math>
-\end{trivlist}
 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