Clausification in Coq

Clausification is an essential step in the so-called resolution method, one of the most successful procedures for automated theorem proving. Anticipating the use of resolution in proof construction systems based on type theory, we elaborate the clausification procedure in Coq and illustrate its usefulness. The results presented in this paper also constitute the formal verification of the correctness of clausification. The complete clausification program and the correctness proof can be found on the following Internet address: http://www.phil.uu.nl/~bezem/Coq/clausification.v 1 Introduction The proof generation capabilities of proof construction systems such as Coq [1], based on type theory, could still be improved. Resolution based theorem provers such as Otter [5] are more powerful in this respect, but have the drawback that they work with normal forms of formulas, so-called clausal forms. Clauses are (universally closed) disjunctions of literals, and a literal is either an atom or ..