Abstract |
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} }
Last modified: Sat Nov 11 20:34:23 CET 2006 |