Automating Meta-Theory Creation and System Extension

In this paper we describe a first experiment with a new approach for building theorem provers that can formalize themselves, reason about themselves, and safely extend themselves with new inference procedures. Within the \tt GETFOL} system we have built a pair of functions that operate between the system's implementation and a theory about this implementation. The first function {\em lifts\/} the actual inference rules to axioms that comprise a theory of {\tt GETFOL}'s inference capabilities. This allows us to turn the prover upon itself whereby we may formally reason about its inference rules and derive new rules. The second function {\em flattens\/ new rules back into the underlying system. This provides a novel means of safe system self-extension and an efficient way of executing derived rules