Jason Hickey and Aleksey Nogin
Accepted to the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004).
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.