Tactic theorem proving with refinement-tree proofs and metavariables

Abstract

This paper describes a prototype of a programmable interactive theorem-proving system. The main new feature of this system is that it supports the construction and manipulation of tree-structured proofs that can contain both metavariables and derived rules that are computed by tactic programs. The proof structure encapsulates the top-down refinement process of proof construction typical of most interactive theorem provers. Our prototype has been implemented in the logic programming language λProlog, from which we inherit a general kind of higher-order metavariable. Backing up, or undoing, of proof construction steps is supported by solving unification and matching constraints.