Sequent Schema for Derived Rules.

Aleksey Nogin and Jason Hickey
Sequent Schema for Derived Rules.
In Victor A. Carreño, Cézar A. Muñoz, and Sophiène Tahar, editors, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), volume 2410 of Lecture Notes in Computer Science, pages 281--297. Springer-Verlag, 2002.
LNCS Entry

Abstract

This paper presents a general sequent schema language that can be used for specifying sequent–style rules for a logical theory. We show how by adding the sequent schema language to a theory we gain an ability to prove new inference rules within the theory itself. We show that the extension of any such theory with our sequent schema language and with any new rules found using this mechanism is conservative.

By using the sequent schema language in a theorem prover, one gets an ability to allow users to derive new rules and then use such derived rules as if they were primitive axioms. The conservativity result guarantees the validity of such approach. This property makes it a convenient tool for implementing a derived rules mechanism in theorem provers, especially considering that the application of the rules expressed in the sequent schema language can be efficiently implemented using MetaPRL's fast rewriting engine.

Back to my publications

Last update: Monday, October 20, 2003 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)