Abstract
The paper describes a generic tool that generates automatically natural language presentations of proofs from various automated and interactive deductive systems. Proofs from different sources are translated into a unified format and equipped with a block structure. These proofs can be easily combined. Several proof transformation procedures, based only on the analysis of structural aspects of the proofs, are available. The tool is part of the ILF system and of the ILF mail server.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Beth, E. W., The Foundations Of Mathematics, North-Holland, 1969
Bibel, W.; Briining, S.; Egly, U.; Rath, T.: KoMeT (system description), Proceedings of the 12th CADE, LNAI 814, pp. 783–787, Springer, 1994
Dahn, B. I.; Gehne, J.; Honigmann, Th.; Walther, L.; Wolf, A.: Integrating Logical Functions with ILF; Preprint 94–10, Humboldt University Berlin, Department of Mathematics
Dahn, B. I.; Wolf, A.: A Calculus Supporting Structured Proofs; Journal for Information Processing and Cybernetics (ElK), 5–6/1994
Denzinger, J., Pitz, W.: Das DISCOUNT-System: Benutzerhandbuch; University of Kaiserslautern, SEKI Working Paper SWP-92–16
Gabbay, D. M.: Labeled Deductive Systems, Vol. 1 - Foundations; MPI-I-94–223, MaxPlanck- Institute Saarbrücken (1994)
Gentzen, G.: Untersuchungen tiber das logische SchlieBen, Mathematische Zeitschrift 39, Berlin, 1935
Huang, X.: Human Oriented Proof Presentation: A Reconstructive Approach, University of the Saarland, SEKI Report SR-94–07
Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W.: SETHEO: A High-Performance Theorem Prover, Journal of Automated Reasoning, 8 (1992)
Letz, R.; Mayr, K.; Goller, Ch.: Controlled Integration of the Cut Rule into Connection Tableau Calculi, Journal of Automated Reasoning, 4 (1994)
Lingenfelder, Ch.: Transformation and Structuring of Computer Generated Proofs, PhD Thesis, Department of Computer Science, University of Kaiserslautern
McCune, W.: Otter 2.0, in: Stickel, M.E. (ed.): Proceedings of the 10th CADE, pp. 663–664, Springer, Berlin, 1990
Pelletier F.J., Rudnicki, P.: Non-Obviousness, In: Wos L. (Ed.), AAR Newsletter (6/1986), Association for Automated Reasoning, Argonne.
Robinson, J. A., A Machine-Oriented Logic Based On The Resolution Principle, Journal ACM 12/1, 1965
Smullyan, R. M., First-Order Logic, Springer, 1968
Stickel, M. E.: A PROLOG Technology Theorem Prover, in: New generation computing 2 (1984)
Suttner, Ch. B.; Sutcliffe, G.: The TPTP Problem Library, Munich University of Technology, Department of Computer Science, Technical Report AR-94–03
Wolf, A.: A Translation of Model Elimination Proofs into an Structured Natural Deduction, to appear
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 Springer Science+Business Media New York
About this chapter
Cite this chapter
Dahn, B.I., Wolf, A. (1996). Natural Language Presentation and Combination of Automatically Generated Proofs. In: Baader, F., Schulz, K.U. (eds) Frontiers of Combining Systems. Applied Logic Series, vol 3. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-0349-4_9
Download citation
DOI: https://doi.org/10.1007/978-94-009-0349-4_9
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-6643-3
Online ISBN: 978-94-009-0349-4
eBook Packages: Springer Book Archive