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.

In Proceedings of the 21st Annual German Conference on Artificial Intelligence (KI'97) Lecture Notes in Artificial Intelligence, Springer-Verlag, 1997. © Springer-Verlag.

gzipped postscript or postscript

BibTeX Entry

@InProceedings{StreckerSorea:KI97,
        TITLE = {Integrating an Equality Prover into a Software Development System Based on Type Theory},
        AUTHOR = {Martin Strecker and Maria Sorea},
        BOOKTITLE = {Proceedings of the 21st Annual German Conference on Artificial Intelligence 
                    (KI'97): Advances in Artificial Intelligence},
        EDITOR = {Gerhard Brewka and Christopher Habel and Bernhard Nebel},
        PAGES = {147--158},
        PUBLISHER = {Springer-Verlag},
        SERIES = {Lecture Notes in Artificial Intelligence},
        VOLUME = 1303,
        MONTH = sep,
        YEAR = 1997,
        ADDRESS = {Berlin}
}