Inference rules: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(Utworzono nową stronę "Inference rules of algorithmic logic \textsc{Inference rules IR} : \begin{trivlist} \item[$R_1$]\qquad $\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }$ \item[$R_{...")
 
(→‎Some auxiliary (secondary) inference rules)
 
(Nie pokazano 10 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 1: Linia 1:
−
Inference rules of algorithmic logic
+
There are seven basic inference rules and much more secondary rules
−
\textsc{Inference rules IR} :
+
== Basic inference rules of algorithmic logic ==
  
 +
<span style="color: Blue"><math>\{R_1\}\qquad\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }  </math></span>
  
−
\begin{trivlist}
+
<span style="color: Blue"><math>\{R_2\}\qquad \dfrac{(\alpha \Rightarrow \beta )}{(K\alpha \Rightarrow K\beta )} </math></span>
−
\item[$R_1$]\qquad $\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }$
+
 
−
\item[$R_{2}$]\qquad $\dfrac{
+
<span style="color: Blue"><math>\{R_3\}\qquad  \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 \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 )} </math></span>
−
\item[$R_{4}$]\qquad  $\dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup
+
 
−
K\alpha \Longrightarrow \beta )}$
+
<span style="color: Blue"><math>\{R_4\}\qquad  \dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup
−
\item[$R_{5}$]\qquad $\dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha
+
K\alpha \Longrightarrow \beta )} </math></span>
−
\Longrightarrow \bigcap K\beta )}$
+
 
−
\item[$R_{6}$]\qquad $\dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists
+
<span style="color: Blue"><math>\{R_5\}\qquad \dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha
−
x)\alpha (x)~\Longrightarrow ~\beta )}$
+
\Longrightarrow \bigcap K\beta )} </math></span>
−
\item[$R_{7}$]\qquad $\dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta
+
 
−
\Longrightarrow (\forall )\alpha (x))}$
+
<span style="color: Blue"><math>\{R_6\}\qquad \dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists
−
\end{trivlist}
+
x)\alpha (x)~\Longrightarrow ~\beta )} </math></span>
−
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
+
<span style="color: Blue"><math>\{R_7\}\qquad \dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta
 +
\Longrightarrow (\forall )\alpha (x))} </math></span>
 +
 
 +
 
 +
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
 
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 $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 '''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 $\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 ''modus ponens'', or the ''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 arbitrary formulas, <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
+
sequence of assignment instructions, and <math>K</math> and <math>M</math> are arbitrary
 
programs.
 
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.<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}\
 +
\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.

Źródło „http://lem12.uksw.edu.pl/index.php?title=Inference_rules&oldid=2267”