Design of a Logic Algorithm

Definition 4-2 A logic algorithm defining a predicate r/n, denoted LA r), is a closed well-formed formula of the form  

In the following, we drop the universal quantifications in front of the heads, as well as any existential quantifications at the beginnings of bodies of logic algorithms. 

Example 4-3 A possible version of LA(compress) is Logic Algorithm 4-1. Example 4-4 A possible version of LA(firstPlateau) is Logic Algorithm 4-2. 

This allows a definition of logic algorithm correctness that is only in terms of the specifications of the used predicates. It establishes an equivalence between the specified relation and the set of Herbrand-logical consequences of the logic algorithm. 

Definition 4-3 Let Specif) be a specification, LA(f) be a logic algorithm, and j be a finite set of logic algorithms containing LA(r). Then LA r) is (totally) correct in Pi wrt Spec(r) iff, for any ground -tuple t, the following two conditions hold  

---

Stage B Design of a logic algorithm (and possibly its transformation) ... 

When a logic algorithm is designed by structural induction on some parameter (as in Chapter 4), then predicate r n can be interpreted in any Herbrand model of LA(r). 

It is interesting to decompose a synthesis process into a series of steps, each designing an intermediate logic algorithm. Indeed ... 

In the case of incremental synthesis, let s view the steps of one synthesis increment as a macro-step performing a transformation trans. Synthesis is then the design of a series of logic algorithms ... 

A possible enhancement is a schema that automatically introduces an additional parameter to the specified predicate, hence covering LA(split) (LA 5-19). Such an extension is discussed by [Summers 77]. This schema could still be considered a design schema, rather than a transformation schema, as it is not possible to design a logic algorithm for split/3 that is covered by one of the given versions. 

Is the mechanism able to design the whole family of possible logic algorithms for a given problem This ability is in theory achieved for the family of algorithms that are covered by version 3 of the divide-and-conquer schema. In practice, everything depends on the completeness of the databases used by Steps 2 and 3. How many structural forms are there Due to our restriction to version 3 of the divide-and-conquer schema. Task C of Step 2 only considers the distinction between two structural forms, namely one minimal form and one non-minimal form. A generalization of this task is considered future research. 

We describe an efficient implementation of a CTL model-checking algorithm based on alternating automata. We use this to check properties of an asynchronous micropipeline design described in the Rainbow framework, which operates at the micropipeline level and leads to compact models of the hardware. We also use alternating automata to characterise die expressive power and model-checking complexity for sub-logics of CTL. ... 

---