Case Studies in Meta-Level Theorem Proving

Proceedings of the 11th International Conference on Theorem Proving in Higher-Order Logics (TPHOLs '98), J. Grundy, M. Newey (Eds.), pp. 461--478, Canberra, Australia, September 1998, volume 1479 of LNCS, © Springer-Verlag.

---

Authors

F.W von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rueß

Abstract

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.

gzipped postscript or postscript

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
 }
 

---

Harald Ruess: ruess@csl.sri.com