Step 4 Syntactic Introduction of the Recursive Atoms

In the non-minimal case, tails TY of Y are obtained by recursion on the tails TX of X. 

The objective at Step 4 is to instantiate the conjunction of recursive atoms of the divide-and-conquer schema. This amounts to transforming LA- r) into LA r) such that it is covered by the following schema  

This amounts to splitting the non-minimal case into two non-mandatory cases, called the non-recursive non-minimal case and the recursive non-minimal case, respectively. For convenience, we drop the qualifier non-minimal from these two names. Recursion may be useless in the sense that the recursively computed TY are not needed for the computation of Y. Useless recursion wouldn t affect the correctness of a logic algorithm, though. Its elimination is thus rather a matter of algorithm optimization. The following objectives of the strategy  

The case splitting and the introduction of a conjunction of recursive atoms into one of the resulting cases are mere syntactic operations, and hence pretty straightforward. 

the decision whether both cases are really necessary is achieved by the following sequence of four tasks  

---

How to detect that recursion is useless in some non-minimal sub-cases Step 4 (Syntactic introduction of the recursive atoms) creates a non-recursive case if at least one example Ej leads to a non-admissible procComp(,,yp atom. Howto invent or re-use appropriate predicates How to implement invented predicates The predicate invention problem is tackled at four points during the synthesis. At Steps 2 and 3, the Database Method re-uses predefined predicates this amounts to using domain knowledge. At Step 6, the Synthesis Method (see Section 14.2.4 below) invents new composition operators. As of now, there is no method yet of re-using common composition operators. At Step 7, the PaP Method synthesizes discriminants that are in terms of predicates other than rfn. How to discover which parameters are auxiliary parameters Due to our restriction to version 3 of the divide-and-conquer schema, auxiliary parameters are not taken into account. See Section 14.2.2 below on how to achieve this. 

---