A transformed version of LP compress-int-L

The remaining, rather technical correctness criteria are specific to every SLDNF refutation procedure. These aspects are usually a simple manual task. They can also be handled by data-flow analysis or abstract interpretation techniques that reveal, for each directionality, a correct permutation of the program clauses, and a correct permutation of the literals in the body of each clause, and sometimes the addition or deletion of literals. Multi-directionality is usually difficult to achieve. The corresponding tool of the Folon environment is described by [De Boeck and Le Charlier 90]. 

The objective of this book is (semi-)automatic logic algorithm synthesis. First, in Section 5.1, we define this objective in more detail and clearly state its boundaries. In order to motivate this research, we develop a series of sample problems in Section 5.2 and show that non-trivial issues have to be solved. This allows us to identify, in Section 5.3, the challenges of logic algorithm synthesis. 

Once the new specification formalism developed, this book is mainly concerned with Stage B, and only marginally with Stage A. 

In order to motivate this research, in Section 5.2.1, we give sample logic algorithms solving some of the problems posed in Section 1.5. Then, in Section 5.2.2, we give some comments on these logic algorithms. 

---