eprover 1.0.004-1ubuntu1 (amd64 binary) in ubuntu karmic
E is a fully automatic theorem prover for full first-order logic with
equality. It accepts a mathematical specification and, optionally, a
hypothesis, and tries to prove the hypothesis and/or find a
saturation representing a (counter-)model for the specification.
.
E is based on a purely equational problem representation and
implements a variant of the superposition calculus. Proof search can
be guided with a multitude of options or a powerful automatic
configuration mode. The system can process input in a number of
different formats, including the standard TPTP-2 and TPTP-3
formats. It can generate proof objects in PCL2 or TPTP-3/TSTP
format.
.
E is considered one of the most powerful and friendly automated
theorem provers for first-order logic. It has consistently been among
the top system in the major categories of the CASC system competition,
and usually been the strongest free software system.
Details
- Package version:
- 1.0.004-1ubuntu1
- Status:
- Obsolete
- Component:
- universe
- Priority:
- Extra
Downloadable files
- eprover_1.0.004-1ubuntu1_amd64.deb (1001.4 KiB)
Package relationships
- Depends on:
- Suggests:
- Recommends: