Back to my publications
Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov
Practical reflection for sequent logics.
In Proceedings of the International Workshop on Logical
Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Electronic
Notes in Theoretical Computer Science, 2006.
PDF.
It is well-known that adding reflective reasoning can tremendously increase the power of a proof assistant. In order for this theoretical increase of power to become accessible to users in practice, the proof assistant needs to provide a great deal of infrastructure to support reflective reasoning. In this paper we explore the problem of creating a practical implementation of such a support layer.Our implementation takes a specification of a logical theory (which is identical to how it would be specified if we simply intended to reason within this logical theory, instead of reflecting it) and automatically generates the necessary definitions, lemmas, and proofs that are needed to enable the reflected meta-reasoning in the provided theory.
One of the key features of our approach is that the structure of a logic is preserved when it is reflected. In particular, all variables, including meta-variables, are preserved in the reflected representation. This also allows the preservation of proof automation—there is a structure-preserving one-to-one map from proof steps in the original logic to proof step in the reflected logic.
To enable reasoning about terms with sequent context variables, we develop a principle for context induction, called teleportation.
This work is fully implemented in the MetaPRL theorem prover.
Last update: Saturday, January 27, 2007 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)