We describe an extension of the PVS system that provides a reasonably efficient and practical notion of reflection and thus allows for soundly adding formalized and verified new proof procedures. These proof procedures work on representations of a part of the underlying logic and their correctness is expressed at the object level using a computational reflection function. The implementation of the PVS system has been extended with an efficient evaluation mechanism, since the practicality of the approach heavily depends on careful engineering of the core system, including efficient normalization of functional expressions. We exemplify the process of applying meta-level proof procedures with a detailed description of the encoding of cancellation in commutative monoids and of the kernel of a BDD package.

Online Copy

Available as Postscript(143 KB) or gzip'ed Postscript (56 KB)

BibTeX Entry

@InProceedings{vHPP+:98, author = "Friedrich W.~von Henke and Stephan Pfab and Holger Pfeifer and Harald Rue{\ss}", title = "{Case Studies in Meta-Level Theorem Proving}", editor = "Jim Grundy and Malcolm Newey", series = "Lecture Notes in Computer Science", number = "1479", pages = "461--478", booktitle = "Proc. Intl. Conf. on Theorem Proving in Higher Order Logics", year = 1998, publisher = "Springer-Verlag", month = sep }