Multi-directionality

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]. 

---