Deductive Generalization and Meta-Reasoning or How to Formalize Genesis

Abstract

When using resolution for showing the unsatisfiability of logic formulas one often encounters infinite sequences of structurally similar clauses. We suggest to use deductive generalization to derive a small number of meta-clauses subsuming these infinite sequences. Resolution is extended by meta-unification in order to resolve meta-clauses instead of ordinary ones. As a step towards a unification procedure for general meta-terms we investigate the unification of monadic ones. We describe an algorithm yielding a finite, complete and orthonormal set of unifiers. First experiments show the usefulness of our approach: theorem provers save space as well as time, proofs become considerably shorter.