Deterministic logic algorithm

Definition 5-2 Let min and max be two scalars. Let LF(r) be the logic program derived from a logic algorithm LA(r), Let r(t) be an atom where the induction parameter and the auxiliary parameter(s) are ground, and all other parameters are variables. We say that LA r) is min - max deterministic iff there are between min and max ground instances of r(t) for which there exists an SLDNF refutation using LP(r). 

The Proofs-as-Programs Method is deterministic because the results of all successful derivations are collected before computing 21 therefrom. The method is thus independent of any ordering of disjuncts within LA r), or of properties within P(r). The method may fail, as conveyed by Definition 9-5. However, nothing can be said about the synthesized logic algorithms in terms of determinism or finiteness, because nothing is known about the properties. 

This algorithm is non-deterministic, finite, and never fails. Moreover, the synthesized logic algorithm is non-deterministic in general, and finite, but may fail. For instance, considering Example 10-2, the atom pcCompress eXe,2]X) is covered by both disjuncts of the synthesized logic algorithm, namely via the answer substitutions X/[e,3] and X/[c,l,, 2]. ... 

Within a restricted setting, the MSG Method infers, from a finite set of general examples, a non-recursive logic algorithm that is defined in terms of the =/2 primitive only, and that is correct wrt a natural extension of the given examples. The underlying algorithm is non-deterministic. 

Note that Steps 2, 3, 5,6 are non-deterministic different logic algorithms can be synthesized upon reconsideration of decisions taken at these steps. 

Finally, the methods of tasks A, C, D are non-deterministic, but finite. This means that choice-points are created there, and that the made selections may be reconsidered later, either because synthesis fails, or because synthesis succeeds and the specifier wants more algorithms. Only Task A could possibly fail, namely if there is no parameter of an inductive type. Do not mix up non-deterministic synthesis and a non-deterministic synthesized algorithm. The latter would feature either mutually nonexclusive cases or predicates that are non-deterministic. The logic algorithm synthesized at Step 2 is deterministic, because the two cases are mutually exclusive by construction, and because the introduced predicates are deterministic. 

Second, note that the methods of both tasks are non-deterministic, finite, and can never fail. However, the introduced predicates are deterministic in the decomposition mode. This implies that the witnesses hxj and txj are unique. The logic algorithm synthesized at Step 3 is thus deterministic. 

Note that the methods of all four tasks are fully deterministic (and thus never fail). Moreover, the logic algorithm synthesized at Step 4 is always deterministic. 

The methods of Tasks M and Q are non-deterministic, finite, and never fail, because of the usage of the ground case of the MSG Method. Moreover, the synthesized instances are non-deterministic and finite, for the same reason. The logic algorithm... 

T. Sato and H. Tamaki. First-order compiler A deterministic logic program synthesis algorithm. J. of Symbolic Computation 8(6) 605-627,1989. 

---