Back to my publicationsJason 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 my TPHOLs'00 presentation: Gzipped PostScript (320KB), PostScript (1005KB)
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.
Last update: Monday, January 26, 2004 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)