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.)
