Toolkit for Construction and Maintenance of Extensible Proof Search Tactics

Опубликовано 6 сентября 2016, 5:08

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. As new axioms, definitions and theorems are added to the system, such tactics may need to be dynamically updated. 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. In my talk I will describe a very general and flexible mechanism for extensible hierarchical tactic construction and maintenance in a logical framework. I will also provide an overview of how this reflective mechanism can be implemented efficiently while requiring little effort from its users. The approaches presented form the core of the tactic construction methodology in the MetaPRL theorem prover, where they have been developed and successfully used for several years. These mechanisms turned out to be very helpful not only in developing automated and interactive proof search techniques, but also in other applications, including development of a reliable extensible compiler.