Integrating an Equality Prover into a Software Development System based on Type Theory

This paper reports on the integration of an untyped equational prover into a proof system based on an expressive constructive type theory. The proofs returned by the equational prover are effectively verified for type correctness, a proof term can be constructed. The scheme of proof translation described here is illustrated by the integration of the Discount prover into the software development system Typelab.
 

Online Copy

Available as Postscript (12 pages, ca 128 KB)
 

BibTeX Entry

@InProceedings{Strecker:97a,
  author =       {Martin Strecker and Maria Sorea},
  title =        {Integrating an Equality Prover into a Software Development
		 System based on Type Theory},
  booktitle =    {Proceedings KI'97},
  editor =       {G. Brewka and Ch. Habel and B. Nebel},
  year =         1997,
  publisher =    {Springer LNAI 1303},
  pages =        {147--158}
}