×

Plagiator – a learning prover. (English) Zbl 1430.68414

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, 256-259 (1997).
For the entire collection see [Zbl 1415.68038].

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Software:

PLAGIATOR; InKa; ABSFOL; KIV
Full Text: DOI

References:

[1] C. Benzmüller et. al. OMEGA: Towards a Mathematical Assistant. In Proc. CADE-14, Townsville, Australia. Springer 1997. · Zbl 1430.68393
[2] J. Brauburger. Plagiator — Design and Implementation of a Learning Prover. Diploma Thesis (in German), TH Darmstadt, 1994.
[3] F. Giunchiglia and A. Villafiorita. ABSFOL: A Proof Checker with Abstraction. In Proc. CADE-13, New Brunswick, USA, pp. 136-140. Springer LNAI 1104, 1996. · Zbl 1412.68226
[4] D. Hutter and C. Sengler. INKA: The Next Generation. In Proc. CADE-13, New Brunswick, USA, pp. 288-292. Springer LNAI 1104, 1996. · Zbl 1412.68236
[5] T. Kolbe and S. Glesner. Many-Sorted Logic in a Learning Theorem Prover. Technical Report IBN 97/43, TH Darmstadt, 1997.
[6] T. Kolbe and C. Walther. Reusing Proofs. In A. Cohn, editor, Proc. ECAI-11, Amsterdam, The Netherlands, pp. 80-84. John Wiley & Sons, Ltd., 1994.
[7] T. Kolbe and C. Walther. Proof Management and Retrieval. In Proceedings of the IJCAI-14 Workshop on Formal Approaches to the Reuse of Plans, Proofs, and Programs, Montreal, Canada, pp. 16-20, 1995.
[8] T. Kolbe and C. Walther. Second-Order Matching modulo Evaluation — A Technique for Reusing Proofs. In Proc. IJCAI-14, Montreal, Canada, pp. 190-195, 1995.
[9] T. Kolbe and C. Walther. Termination of Theorem Proving by Reuse. In Proc. CADE-13, New Brunswick, USA, pp. 106-120. Springer LNAI 1104, 1996. · Zbl 1412.68241
[10] W. Reif, G. Schellhorn and K. Stenzel. Proving System Correctness with KIV 3.0. In Proc. CADE-14, Townsville, Australia. Springer 1997.
[11] C. Walther. Mathematical Induction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, pp. 127-227. Oxford University Press, 1994.
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.