Logic algorithm schema

Example 8-1 Here is a logic algorithm schema for the generate-and-test strategy ... 

A wff schema language is thus needed to write realistic logic algorithm schemas. The formal definition of such a language and of its semantics is beyond the scope of this book, so we do not develop it. But we know from experience that the intuitive understanding of our schemata is sufficient. 

Definition 8-1 A logic algorithm schema is a closed wff schema of the form ... 

Hereafter, we drop the universal quantifications in front of the heads, as well as any existential quantifications at the beginning of the bodies of logic algorithm schemas. 

It is evident that a logic algorithm schema without function-variables, predicate-variables, and schema-variables is a logic algorithm. 

Definition 8-2 An instance of a logic algorithm schema is a logic algorithm obtained by the following sequence of operations ... 

Logic Algorithm Schema 8-1 Divide-and-conquer (version 1)... 

First, in view of having a theoty of logic algorithm schemas and a formalization of the accompanying notions of instantiation and classification, a language for wff schemas needs to be developed, as well as its semantics defined. 

The presented synthesis mechanism is guided by version 3 of the divide-and-conquer logic algorithm schema. This preliminary restriction (made in Section 11.2) has considerably simplified the notations needed for the theoretical presentation. The support of version 4 (relations of any non-zero arity) is actually a pretty straightforward extension, because only some additional vectorization is needed. Version 4 is actually supported by the implementation of the synthesis mechanism. 

Connectives for logic algorithms, schemas, properties, and implicative goals ... 

---