A Non-Incremental Synthesis Strategy

Example 7-9 LA fsum) is a better complete approximation of Sum than LA/ft sum). 

A first idea of a non-incremental stepwise synthesis strategy (with a fixed, finite number /of predefined steps) is to achieve downward progression  

In such a non-incremental synthesis, the series of expanded logic algorithms can be shown to progress upwards (see below). To achieve this expansion, we here only consider logic algorithms whose bodies are in disjunctive normal form. The used predicates are assumed to be either primitives or the predicate rhi that is defined by the logic algorithm. Let s start with a few basic definitions. 

Definition 7-21 LtiD[X] be a disjunct of a logic algorithm LA(r), such that the only free variables of D are the n universal variables X in the head of LA r), We say that D[X] covers atom r t) iff 3D[t] is true in 3. 

Example 7-11 The first disjunct of LA sum) covers the example 5wm([],0). Its second disjunct covers the example 5w/n([7],7), but it doesn t cover sum([],0). 

---