Abstract
Ilf is a convenient interface between the non-expert user of ATP's and most of the available high performance ATP's. The typed first order input language and the transformation algorithms for coding types into clausal logic, which are integrated into Ilf, make ATP's almost transparent to the user. One only has to learn one language to use many provers. The natural language proof presentation unit closes the gap between the (illegible) machine output of ATP's and the desire of the user to understand machine generated proofs. It is planned to upgrade all integrated ATP's as well as to integrate new high performance provers.
This work is supported by the Deutsche Forschungsgemeinschaft within the Schwerpunkt Deduktion and the Sonderforschungsbereich 342, subproject A5.
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.
Similar content being viewed by others
References
J. Avenhaus, J. Denzinger, and Matt. Fuchs. DISCOUNT: A System For Distributed Equational Deduction. In Proc. 6, RTA, pp. 397–402, Springer, 1995.
W. Bibel, S. Brüning, U. Egly, and T. Rath. KoMeT, system description. In Proc. CADE-12, pp. 783–787, Springer, 1994.
B. I. Dahn, J. Gehne, Th. Honigmann, L. Walther, and A. Wolf. Integrating Logical Functions with Ilf. TR 94-10, Humboldt Univ. Berlin, Math. Dept., 1994.
B. I. Dahn and A. Wolf. A Calculus Supporting Structured Proofs. Journal for Information Processing and Cybernetics (EIK), (5–6): pp. 261–276, 1994.
B. I. Dahn and A. Wolf. Natural Language Presentation and Combination of Automatically Generated Proofs. In Proc. FroCoS'96, pp. 175–192, Kluwer, 1996.
C. Goller, R. Letz, K. Mayr, and J. Schumann. SETHEO V3.2: Recent Developments (System Abstract). In Proc. CADE-12, pp. 778–782, Springer, 1994.
W. McCune. Otter 2.0. In Proc. CADE-10, pp. 663–664, Springer, 1990.
C. S. Mellish. Implementing systemic classification by unification. Comp. Ling., 14:40–51, 1988.
G. Sutcliffe, C.B. Suttner, and T. Yemenis. The TPTP Problem Library. In Proc. CADE-12, pp. 252–266, Springer, 1994.
C. Weidenbach, B. Gaede, and G. Rock. Spass & flotter, version 0.42. In Proc. CADE-13, pp. 141–145, Springer, 1996.
A. Wolf and J. Schumann. ILF-SETHEO. In Proc. CADE-14, accepted paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dahn, B.I., Gehne, J., Honigmann, T., Wolf, A. (1997). Integration of automated and interactive theorem proving in ILF. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_7
Download citation
DOI: https://doi.org/10.1007/3-540-63104-6_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63104-0
Online ISBN: 978-3-540-69140-2
eBook Packages: Springer Book Archive