Inference rules: Różnice pomiędzy wersjami
(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_{...") |
(Brak różnic)
|
Wersja z 09:32, 19 lis 2015
Inference rules of algorithmic logic \textsc{Inference rules IR} :
\begin{trivlist}
\item[$R_1$]\qquad $\dfrac{\alpha ,(\alpha \Rightarrow \beta )}{\beta }$
\item[$R_{2}$]\qquad $\dfrac{
(\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 )}$
\item[$R_{4}$]\qquad $\dfrac{\{(K^i\alpha \Longrightarrow \beta )\}_{i\in N}}{(\bigcup
K\alpha \Longrightarrow \beta )}$
\item[$R_{5}$]\qquad $\dfrac{\{(\alpha \Longrightarrow K^i\beta )\}_{i\in N}}{(\alpha
\Longrightarrow \bigcap K\beta )}$
\item[$R_{6}$]\qquad $\dfrac{(\alpha (x)~\Longrightarrow ~\beta )}{((\exists
x)\alpha (x)~\Longrightarrow ~\beta )}$
\item[$R_{7}$]\qquad $\dfrac{(\beta ~\Longrightarrow ~\alpha (x))}{(\beta
\Longrightarrow (\forall )\alpha (x))}$
\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
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.
