Fast Tactic-Based Theorem Proving
by Jason Hickey, Aleksey Nogin
Proceedings of 13th International Conference (TPHOLs 2000), LNCS 1869, pp. 252-266, Springer-Verlag
Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose meta-language to implement both general-purpose reasoning and computationally intensive domain-specific proof procedures. The generality of tactic provers has a performance penalty; the speed of proof search lags far behind special-purpose provers. We present a new modular proving architecture that significantly increases the speed of the core logic engine. Our speedup is due to efficient data structures and modularity, which allows parts of the prover to be customized on a domain-specific basis. Our architecture is used in the MetaPRL logical framework, with speedups of more than two orders of magnitude over traditional tactic-based proof search.
bibTex ref: HN00