Back to my publicationsJason Hickey and Aleksey Nogin
Extensible Hierarchical Tactic Construction in a Logical Framework.
In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors,
Proceedings of the 17th International Conference on Theorem Proving in
Higher Order Logics (TPHOLs 2004), volume 3223 of Lecture Notes in
Computer Science, pages 136--151. Springer-Verlag, 2004.
PDF
(244KB), PostScript
(202KB)
Theorem provers for higher-order logics often use tactics to implement automated proof search. Often some basic tactics are designed to behave very differently in different contexts. Even in a prover that only supports a fixed base logic, such tactics may need to be updated dynamically as new definitions and theorems are added. In a logical framework with multiple (perhaps conflicting) logics, this has the added complexity that definitions and theorems should only be used for automation only in the logic in which they are defined or proved.
This paper describes a very general and flexible mechanism for extensible hierarchical tactic maintenance in a logical framework. We also explain how this reflective mechanism can be implemented efficiently while requiring little effort from its users.
The approaches presented in this paper form the core of the tactic construction methodology in the MetaPRL theorem prover, where they have been developed and successfully used for several years.
Last update: Friday, October 22, 2004 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)