Preview
Unable to display preview. Download preview PDF.
References
O.L. Astrachan and D.W. Loveland. The Use of Lemmas in the Model Elimination Procedure. Journal of Automated Reasoning, 19(1):117–141, 1997.
M. Fuchs. Controlled Use of Clausal Lemmas in Connection Tableau Calculi. AR-Report, AR-98-02, TU München.
M. Fuchs. Flexible proof replay with heuristics. In Proc. EPIA-97, LNAI 1323, pages 1–12. Springer, 1997.
R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, (13):297–337, 1994.
D.W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8(2):183–212, 1992.
S. Minton. Quantitative Results Concerning the Utility of Explanation-Based Learning. Artificial Intelligence, (42):363–391, 1990. Elsevier Science Publishers.
J. Schumann. Delta — a bottom-up preprocessor for top-down theorem provers. In Proc. CADE-12. Springer, 1994.
M.E. Stickel. A prolog technology theorem prover: Implementation by an extended prolog compiler. Journal of Automated Reasoning, 4:353–380, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fuchs, M. (1998). System description: similarity-based lemma generation for model elimination. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054243
Download citation
DOI: https://doi.org/10.1007/BFb0054243
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64675-4
Online ISBN: 978-3-540-69110-5
eBook Packages: Springer Book Archive