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.
This research has partly been supported by the “Deutsche Forschungsgemeinschaft” within the “Schwerpunktprogramm Deduktion”
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Bruno Barras et al. The Coq Proof Assistant Reference Manual, Version 6.1. INRIA Rocquencourt and CNRS-ENS Lyon, November 1996.
Bernhard Beckert, Reiner Hänle, Karla Geiß, Peter Oel, Christian Pape, and Martin Sulzmann. The many-valued tableau-based theorem prover 3 TAP, version 4.0. Interner Bericht 3/96, Universität Karlsruhe, Fakultät für Informatik, 1996.
R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.
Bernd I. Dahn, Jürgen Gehne, Thomas Honigmann, Lutz Walther, and Andreas Wolf. Integrating Logical Functions with ILF. Humboldt-Universität Berlin, 1995.
J. Denzinger, M. Kronenburg, and S. Schulz. Discount-a distributed and learning equational prover. Journal of Automated Reasoning, 1997. To appear.
M. Heisel, W. Reif, and W. Stephan. Implementing verification strategies in the KIV-System. In Proc. 9th CADE, pages 131–140. Springer LNCS 310, 1988.
John Harrison and Laurent Théry. Extending the HOL theorem prover with a computer algebra system to reason about the reals. In Jeffrey J. Joyce and Carl Seger, editors, Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, volume 780 of Lecture Notes in Computer Science, pages 174–184, UBC, Vancouver, Canada, 1993. Springer-Verlag.
Christoph Kreitz, Jens Otten, and Stephan Schmitt. Guiding program development systems by a connection based proof strategy. In LoPSTr'95: Proceedings of the 5th International Workshop on Logic Program Synthesis and Transformation, pages 137–151. Springer LNCS 1048, 1996.
Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, July 1990.
S. Owre, N. Shankar, and J.M. Rushby. The PVS Specification Language. Computer Science Lab, SRI International, Menlo Park CA 94025, March 1993.
Larry Paulson. Isabelle — a generic theorem prover. Springer LNCS 828, 1994.
Maria Sorea. Integration von Gleichheitsbeweisen in einen typentheoretischen Beweiser. Master's thesis, Universität Ulm, 1996.
F.W. von Henke, M. Luther, and M. Strecker. Typelab: An environment for modular program development. In M. Dauchet M. Bidoit, editor, Proceedings TAPSOFT'97, pages 851–854. Springer LNCS 1214, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Strecker, M., Sorea, M. (1997). Integrating an equality prover into a software development system based on type theory. In: Brewka, G., Habel, C., Nebel, B. (eds) KI-97: Advances in Artificial Intelligence. KI 1997. Lecture Notes in Computer Science, vol 1303. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540634932_11
Download citation
DOI: https://doi.org/10.1007/3540634932_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63493-5
Online ISBN: 978-3-540-69582-0
eBook Packages: Springer Book Archive