E equational theorem prover
From Wikipedia, the free encyclopedia
E is a modern, high performance theorem prover for full first-order logic with equality. It has been developed primarily in the Automated Reasoning Group at TU Munich.
The system is based on the equational superposition calculus. In contrast to most other current provers, the implementation actually uses a purely equational paradigm, and simulates non-equational inferences via appropriate equality inferences. Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation), several efficient indexing data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour.
E is implemented in C and portable to most UNIX dialects. It is available under the GNU GPL and can be downloaded from the home page linked below.
[edit] References
- Schulz, Stephan (2002). "E - A Brainiac Theorem Prover". Journal of AI Communications 15 (2/3): 111-126.
- Schulz, Stephan (2004). System Description: E 0.81. Proceedings of the 2nd International Joint Conference on Automated Reasoning, Springer LNAI 3097.
[edit] External links
 |
This software-related article is a stub. You can help Wikipedia by expanding it. |
