11. Two programs for logical conversion

The program in Section 11.1 transforms a formula in first-order Predicate Logic to clausal form, as described in Section 2.5. The program in Section 11.2 completes a given set of general clauses by means of Predicate Completion (Section 8.2). The output of this program is a formula in Predicate Logic, which can be transformed back to clausal form by means of the first program.