We describe the main characteristics of version 0.3 of the E equational theorem prover. E is based on superposition and rewriting. It features a powerful interface for specifying search guiding heuristics. We discuss some important details of the implementation and demonstrate the performance of the prover by presenting experimental results on the TPTP. Finally, we describe our future plans for improving the system.
CITATION STYLE
Schulz, S. (1999). System abstract: E 0.3. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1632, pp. 297–301). Springer Verlag. https://doi.org/10.1007/3-540-48660-7_27
Mendeley helps you to discover research relevant for your work.