Bug#521918: RFS: eprover 1.0.004-2 - Theorem prover for first-order logic with equality
Petr Pudlak
deb at pudlak.name
Sat May 9 06:59:34 UTC 2009
Hi,
I'm looking for a sponsor to upload an updated version 1.0.004-2 of the
package. There are just minor changes from version 1.0.004-1:
- Fixed FTBFS when calling pbuilder with --binary-arch (see bug #521918).
- Removed unnecessary dependencies from debian/control.
The package should be lintian clean and build under pbuilder.
The package is available at
http://git.debian.org/?p=debian-science/packages/eprover.git
The long description of the package:
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.
Thanks in advance,
Petr
More information about the debian-science-maintainers
mailing list