Sciweavers

TPHOL
2000
IEEE

Fast Tactic-Based Theorem Proving

14 years 4 months ago
Fast Tactic-Based Theorem Proving
Theorem provers for higher-order logics often use tactics to implement automated proof search. Tactics use a general-purpose metalanguage 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.
Jason Hickey, Aleksey Nogin
Added 01 Aug 2010
Updated 01 Aug 2010
Type Conference
Year 2000
Where TPHOL
Authors Jason Hickey, Aleksey Nogin
Comments (0)