Abstract
We describe the main characteristics of version 0.61 of the E equational theorem prover. E is based on superposition (with literal selection) and rewriting. A particular strength of E is the ability to control the proof search very well. This is reflected by a very powerful and flexible interface for the specification of clause selection functions, and by a wide variety of functions for the selection of inference literals. We discuss some important aspects of the implementation and demonstrate the performance of the prover by presenting experimental results on the TPTP. Finally, we describe our future plans for the system.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
J. Avenhaus, T. Hillenbrand, and B. Löchner. On Using Ground Joinable Equations in Equational Theorem Proving. Proc. of the 3rd FTP, St. Andrews, Scottland, Fachberichte Informatik. Universität Koblenz-Landau, 2000. (revised version submitted to the JSC).
L. Bachmair and H. Ganzinger. Rewrite-Based Equational Theorem Proving with Selection and Simplification. Journal of Logic and Computation, 3(4):217–247, 1994.
J. Denzinger, M. Kronenburg, and S. Schulz. DISCOUNT: A Distributed and Learning Equational Prover. Journal of Automated Reasoning, 18(2):189–198, 1997.
S. Schulz. System Abstract: E 0.3. Proc. of the 16th CADE, Trento, LNAI 1632, 297–391. Springer, 1999.
S. Schulz. The E Web Site. http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/-eprover.html, 1999.
S. Schulz. The E Equational Theorem Prover-User Manual. Automated Reasoning Group, Institut für Informatik, TU Mönchen, 2001. (to appear).
S. Schulz. Learning Search Control Knowledge for Equational Deduction. DISKI 230. Akademische Verlagsgesellschaft Aka GmbH Berlin, 2000.
G. Sutcliffe, C.B. Suttner, and T. Yemenis. The TPTP Problem Library. Proc. of the 12th CADE, Nancy, LNAI 814, 252–266. Springer, 1994.
G. Sutcliffe. The CADE-17 ATP System Competition. Journal of Automated Reasoning, 2001 (to appear).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schulz, S. (2001). System Abstract: E 0.61. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_28
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive