Letter

E - Equational Theorem Prover

Website: http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
License: GPLv2
Vendor: Fedora Project
Description:
E is a purely equational theorem prover for full first-order logic.
That means it is a program that you can stuff a mathematical specification
(in first-order format) and a hypothesis into, and which will then run
forever, using up all of your machines' resources.
Very occasionally it will find a proof for the hypothesis and tell you so.

E's inference core is based on a modified version of the superposition
calculus for equational clausal logic.  Both clausification and reasoning on
the clausal form can be documented in checkable proof objects.

E was the best-performing open source software prover in the 2008
CADE ATP System Competition (CASC) in the FOF, CNF, and UEQ divisions.

Packages

E-1.0.002-4.fc11.ppc64 [1.0 MiB] Changelog by Fedora Release Engineering (2009-02-23):
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild

Listing created by Repoview-0.6.3-1.fc11