| Paketname | eprover |
| Beschreibung | Theorem prover for first-order logic with equality |
| Archiv/Repository | Offizielles Ubuntu Archiv lucid (universe) |
| Version | 1.0.004-1ubuntu1 |
| Sektion | universe/science |
| Priorität | extra |
| Installierte Größe | 2040 Byte |
| Hängt ab von | libc6 (>= 2.4) |
| Empfohlene Pakete | eprover-doc-html |
| Paketbetreuer | Ubuntu MOTU Developers |
| Quelle | |
| Paketgröße | 945562 Byte |
| Prüfsumme MD5 | 27cdc0fd1a6142465ef5d413fc86dafb |
| Prüfsumme SHA1 | 11de57bf94e8e3e5842a7ab8a879c541ab1e5da6 |
| Prüfsumme SHA256 | 4b1f55e1ea0e6d84e104688f2534f05499028af862932dfac27be8ce828e9f3d |
| Link zum Herunterladen | eprover_1.0.004-1ubuntu1_i386.deb |
| Ausführliche Beschreibung | 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.
|