Step 7 Synthesis of the Discriminate

An instantiation of the Discriminate predicate-variable tests the values of HX, TX, Y to see whether SolveNonMinj, respectively Process/ a Compose), is applicable. 

The objective at Step 7 is to instantiate the predicate-variables Discriminate of the divide-and-conquer schema. This amounts to transforming LA r) into LA-j r) such that it is covered by the following schema  

Step 7 should be totally independent of the choice of Step 6 to merge the processj and compose/ predicates. 

Heuristic 13-3 From the used divide-and-conquer schema, we know that the parameters of the discriminate are HX, TX, and T, so we should project [Pettorossi and Proietti 89] the discriminants upon these parameters. 

Heuristic 13-4 If parameter T is not an auxiliary parameter (see Section 14.2.2 on how to detect auxiliary parameters), then it is irrelevant for discrimination, and its equality atom may be deleted from the body of every discriminant. 

---

How to discriminate between these sub-cases Step 7 (Synthesis of the Discriminate achieves this by using the PaP Method. 

Note that E and L are auxiliary parameters. The synthesis of LA compress) proceeds to Step 7 (Synthesis of the Discriminate, where an LA-j(compress) is found that is equivalent to LA (compress). ... 

Note that if properties could also be equivalence statements rather than only definite clauses, then properties would actually be a generalization of negative examples, because they would then embody conditions about when the intended relation does not hold. Most properties are actually equivalence statements. For instance, all properties in the sample specifications of Section 6.2, except for the informative property P2 of EP(efface), would also be correct if they were equivalences. The current version of the synthesis mechanism would only use the //parts of such extended properties in Step 7 for the synthesis of the discriminants. But an extended version performing the above-mentioned over-generalization-check could use the only-if parts to infer negative examples, rather than relying on their explicit presence in the specification. 

This completes Step 6, and the synthesis of LA(r) proceeds to Step 7, where a true discriminant is synthesized because the information of the properties of r n is inherited by the properties of procComp, and is thus already accounted for. 

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. 

---