# Fast Tactic-based Theorem Proving.

Jason Hickey and Aleksey Nogin.

**Fast tactic-based theorem proving.**

In J. Harrison and M. Aagaard, editors, *Theorem Proving in
Higher Order Logics: 13th International Conference, TPHOLs 2000*, volume 1869
of *Lecture Notes in Computer Science*, pages 252-266.
Springer-Verlag, 2000:

PDF (264KB), Gzipped PostScript (367KB), PostScript (815KB)

Slides from the TPHOLs'00 presentation: Gzipped PostScript (320KB), PostScript (1005KB)

## Abstract

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.