×

Integration of automated and interactive theorem proving in ILF. (English) Zbl 1430.68397

McCune, William (ed.), Automated deduction – CADE-14. 14th international conference on automated deduction, Townsville, North Queensland, Australia. July 13–17, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1249, 57-60 (1997).
Summary: 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.
For the entire collection see [Zbl 1415.68038].

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] J. Avenhaus, J. Denzinger, and Matt. Fuchs. DISCOUNT: A System For Distributed Equational Deduction. In Proc. 6, RTA, pp. 397-402, Springer, 1995.
[2] W. Bibel, S. Brüning, U. Egly, and T. Rath. KoMeT, system description. In Proc. CADE-12, pp. 783-787, Springer, 1994. · Zbl 1433.68535
[3] 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. · Zbl 1430.68397
[4] B. I. Dahn and A. Wolf. A Calculus Supporting Structured Proofs. Journal for Information Processing and Cybernetics (EIK), (5-6): pp. 261-276, 1994. · Zbl 0837.03011
[5] B. I. Dahn and A. Wolf. Natural Language Presentation and Combination of Automatically Generated Proofs. In Proc. FroCoS’96, pp. 175-192, Kluwer, 1996. · Zbl 0894.68136
[6] 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.
[7] W. McCune. Otter 2.0. In Proc. CADE-10, pp. 663-664, Springer, 1990. · Zbl 1509.68312
[8] C. S. Mellish. Implementing systemic classification by unification. Comp. Ling., 14:40-51, 1988.
[9] G. Sutcliffe, C.B. Suttner, and T. Yemenis. The TPTP Problem Library. In Proc. CADE-12, pp. 252-266, Springer, 1994. · Zbl 1433.68569
[10] C. Weidenbach, B. Gaede, and G. Rock. Spass & flotter, version 0.42. In Proc. CADE-13, pp. 141-145, Springer, 1996. · Zbl 1412.68267
[11] A. Wolf and J.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.