Hi,

as I was suggested, I'm looking for a sponsor for the "eprover" package, who 
would help me with publishing the package. (http://bugs.debian.org/516545). I 
believe that Debian Science would be a proper place for it. As advised, I 
obtained a more proper description:

Description: Theorem prover for first-order logic with equality
 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.

My packages can be found at https://petr.pudlak.name/deb/
Lintian doesn't complain.

I must admit that some maintainers at the debian-mentors list weren't
too happy with the man pages. At this point they  are more or  less 
just created using help2man and probably I can't do better in near future.
(See the discussion at
 http://lists.debian.org/debian-mentors/2009/02/threads.html#00211 )
However, the package includes more thorough PDF documentation
from the upstream author.

Thanks for help,
  Petr


On Sunday 22 February 2009 14:10:11 Andreas Tille wrote:
> Hi,
>
> this seems like a nce target for Debian Science Mathematics
> section.  Petr, do you consider putting the package under
> Debian Science team maintenance?
>
> Kind regards
>
>        Andreas.
>
> On Sun, 22 Feb 2009, Petr Pudlak wrote:
> > Package: wnpp
> > Severity: wishlist
> > Owner: Petr Pudlak <d...@pudlak.name>
> >
> >
> > * Package name    : eprover
> >  Version         : 1.0.004
> >  Upstream Author : Stephan Schulz <sch...@eprover.org>
> > * URL             : http://www.eprover.org/
> > * License         : GPL-2
> >  Programming Lang: C
> >  Description     : The Equational Theorem Prover E
> >
> > E is an automated equational theorem prover. That means it is a program
> > that you can stuff a mathematical specification (in first-order logic
> > with equality) 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 ;-).
> >
> > Release 1.0 is the culmination of a long development phase. Important
> > changes vs. version 0.999 include the fixing of some bugs in definitional
> > clausification for large problems and general cleanup.
> >
> > (Copied from the original documentation.)

Reply via email to