Proving Ground Completeness of Resolution by Proof Planning

Abstract

A lot of the human ability to prove hard mathematical theorems can be ascribed to a problem-specific problem solving know-how. Such knowledge is intrinsically incomplete. In order to prove related problems human mathematicians, however, can go beyond the acquired knowledge by adapting their know-how to new related problems. These two aspects, having rich experience and extending it by need, can be simulated in a proof planning framework: the problem-specific reasoning knowledge is represented in form of declarative planning operators, called methods; since these are declarative, they can be mechanically adapted to new situations by so-called meta-methods. In this contribution we apply this framework to two prominent proofs in theorem proving, first, we present methods for proving the ground completeness of binary resolution, which essentially correspond to key lemmata, and then, we show how these methods can be reused for the proof of the ground completeness of lock resolution.