(apx:b)= # Two programs for logical conversion # The program in {numref}`Section %s` transforms a formula in first-order Predicate Logic to clausal form, as described in {numref}`sec:2.5`. The program in {numref}`Section %s` completes a given set of general clauses by means of Predicate Completion ({numref}`sec: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.