University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Our Papers

Case Studies in Meta-Level Theorem Proving

F.W. von Henke, S. Pfab, H. Pfeifer, H. Rueß

Proc. Intl. Conf. on Theorem Proving in Higher Order Logics TPHOLs'98
Springer LNCS, Vol. 1479, Sept. 1998
© Springer-Verlag


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

  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

Dept. of AI Homepage Research Help Mail to Webmaster H. Pfeifer - June 28, 1998