Clausification in Coq

Abstract

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.