Procedure

In the paper [BDFL02] a method for solving the ground induction problem was proposed and its completeness for the case of monodic specifications was established. We decsribe here a procedure, implementing this method, applicable to all the temporal specifications defined above.

The problem.

Given: A temporal specification $SP = <\mathcal{U},\mathcal{S},\mathcal{T}>$
with $\mathcal{T}= \{ \forall \bar{x} (\varphi_{1}(\bar{x}) \rightarrow \chi_{1}(\bar{x})), \ldots, \varphi_{k}((\bar{x}) \rightarrow \chi_{k}(\bar{x}) \})$ and a first-order formula $\psi$ Decide: Is $SP \rightarrow \raisebox{-.2ex}{ \mbox{\unitlength=0.9ex \begin{picture}(2,... ... \put(0,0){\line(0,1){2}} \put(2,0){\line(0,1){2}} \end{picture}}} \psi$ valid ?

The procedure.

Stage 1. Saturation of the universal part
$\mathcal{U}_{1} := \mathcal{U}$; $\mathcal{U}_{2} := \emptyset$;
while $(\mathcal{U}_{1} \not= \mathcal{U}_{2})$ do
{
$\mathcal{U}_{2} := \mathcal{U}_{1}$;
for all subsets $\{i_{1}, \ldots i_{l}\} \subseteq \{1,2, \ldots k \}$
do
{
if $\mathcal{U}_{1} \cup \{\forall \bar{x} (\chi_{i_{1}}(\bar{x}) \vee \ldots \vee \chi_{i_{1}}(\bar{x})) \} \vdash \bot$
then $\mathcal{U}_{1} := \mathcal{U}_{1} \cup \{ \neg \forall \bar{x} (\varphi_{i_{1}}(\bar{x}) \vee \ldots \vee \varphi_{i_{1}}(\bar{x}))\}$ ;
if $\mathcal{U}_{1} \cup \{\exists \bar{x} (\chi_{i_{1}}(\bar{x}) \land \ldots \land \chi_{i_{1}}(\bar{x})) \} \vdash \bot$
then $\mathcal{U}_{1} := \mathcal{U}_{1} \cup \{ \neg \exists \bar{x} (\varphi_{i_{1}}(\bar{x}) \land \ldots \land \varphi_{i_{1}}(\bar{x}))\}$;
}
} Stage 2. Checking the start conditions
if $\mathcal{S}\land \mathcal{U}_{1} \not\vdash \psi$ then STOP with answer ``No'' ;
else Continue; Stage 3. Generation of merged rules
$M := \emptyset$
for all subsets $\{i_{1}, \ldots i_{l}\} \subseteq \{1,2, \ldots k \}$
do
{
if ( $\mathcal{U}_{1} \cup \{\exists \bar{x} ((\chi_{i_{1}}(\bar{x}) \land \ldots \land \chi_{i_{1}}(\bar{x}))\}\vdash \psi)$
then $M : = M \cup \{\exists \bar{x} (\varphi_{i_{1}}(\bar{x}) \land \ldots \land \... ... \bar{x} (\chi_{i_{1}}(\bar{x}) \land \ldots \land \chi_{i_{l}}(\bar{x})))\};$
if ( $\mathcal{U}_{1} \cup \{\forall \bar{x} ((\chi_{i_{1}}(\bar{x}) \vee \ldots \vee \chi_{i_{1}}(\bar{x}))\}\vdash \psi)$
then $M : = M \cup \{\forall \bar{x} (\varphi_{i_{1}}(\bar{x}) \vee \ldots \vee \va... ...bar{x} (\chi_{i_{1}}(\bar{x}) \vee \ldots \vee \chi_{i_{l}}(\bar{x}))) \};$
} Stage 4. Checking the loop conditions
for all subsets $\{Q_{i_{1}}\bar{x} \varphi_{i_{1}} \rightarrow \!\raisebox{-.2ex}{ \mbox{\unitl... ...h \par\end{picture}}} Q_{i_{l}}\bar{x} \chi_{i_{l}}(\bar{x}) \} \subseteq M$ ( $Q_{i_{k}} \in \{\forall , \exists\}$)
do
{
if $\mathcal{S}\land \mathcal{U}\vdash \exists \bar{x} (\bigvee_{j=1}^{l}\varphi_{i_{j}}(\bar{x}))$ and $\forall j \in \{1, \ldots l\} \mathcal{U}\vdash (\forall \bar{x} \exists \ba... ..._{i_{j}}(\bar{x}) \rightarrow \bigvee_{k = 1}^{l} \varphi_{i_{k}}(\bar{z})))$
then STOP with answer ``Yes''
}
STOP with answer ``I don't know''.

The procedure is correct in the following sense: if it stops and produces the answer "Yes" then, indeed, $SP \rightarrow \raisebox{-.2ex}{ \mbox{\unitlength=0.9ex \begin{picture}(2,... ... \put(0,0){\line(0,1){2}} \put(2,0){\line(0,1){2}} \end{picture}}} \psi$ is valid (by straightforward check, see [BDFL02]). However, in general it is incomplete and may produce an ``I don't know'' answer for a valid formula. In the case of monodic specifications it is complete modulo first-order derivability, i.e. if one assumes the existense of oracle resolving the tasks of the kind $\rho_{1} \vdash \rho_{2}$ for the first-order formulae $\rho_{1}$ and $\rho_{2}$. To obtain the complete procedure in the case of real semi-decision (proof search) procedures for first-order logic, one needs to apply special strategies, ensuring the (uniform) progress in the proof search for all first-order formulae generated.