Reflection of Formal Tactics in a Deductive Reflection Framework

Presented at CADE'96, New Brunswick, NJ, August 1996. © Springer-Verlag.

---

Authors

Harald Rueß

Abstract

Tactics are encoded as verifiable meta-functions in a powerful programming logic with reflective capabilities. These formalized tactics are applied to specific problems by means of deductive reflection rules. The main advantage of this approach lies in the fact that meta-theoretic results, once proven, are used without further justification to construct proofs of object-level problems. As another consequence, new theorem-proving capabilities like decision procedures are added and tightly integrated with the basic formal tactics mechanism in a sound way.

gzipped postscript or postscript

BibTeX Entry

@InProceedings{Ruess:CADE96,
  author =       {Harald Rue{\ss}},
  title =        {Reflection of formal tactics in a deductive reflection framework},
  pages =        {628--642},
  ISBN =         {3-540-61511-3},
  editor =       {M. A. McRobbie and J. K. Slaney},
  booktitle =    {Proceedings of the Thirteenth International Conference on Automated Deduction ({CADE}-96)},
  month =        {July/August},
  series =       LNAI,
  volume =       1104,
  publisher =    {Springer-Verlag},
  address =      Berlin,
  year =         1996,
}

---

Harald Ruess: ruess@csl.sri.com