FAQ Search Today's Posts Mark Forums Read
» Video Reviews

» Linux Archive

Linux-archive is a website aiming to archive linux email lists and to make them easily accessible for linux users/developers.


» Sponsor

» Partners

» Sponsor

Go Back   Linux Archive > Debian > Debian Development

 
 
LinkBack Thread Tools
 
Old 02-22-2009, 07:57 AM
Petr Pudlak
 
Default Bug#516545: ITP: eprover -- The Equational Theorem Prover E

Package: wnpp
Severity: wishlist
Owner: Petr Pudlak <deb@pudlak.name>


* Package name : eprover
Version : 1.0.004
Upstream Author : Stephan Schulz <schulz@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.)

-- System Information:
Debian Release: 5.0
APT prefers testing
APT policy: (990, 'testing'), (500, 'stable'), (150, 'unstable')
Architecture: i386 (i686)



--
To UNSUBSCRIBE, email to debian-devel-REQUEST@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact listmaster@lists.debian.org
 
Old 02-22-2009, 02:18 PM
Guus Sliepen
 
Default Bug#516545: ITP: eprover -- The Equational Theorem Prover E

On Sun, Feb 22, 2009 at 09:57:04AM +0100, Petr Pudlak wrote:

> * Package name : eprover
> Description : The Equational Theorem Prover E

That is not a description, that is just the name spelled out. A better
description would be "equational theorem prover".

> 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,

So far so good...

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

If I read this, I think: "What kind of crap software is this that suffers from
infinite loops and only works for only a handful of equations? Why is it in
Debian if there are other theorem provers that are apparently better?"

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

That information belongs in the upstream NEWS or Changes file, not in a package
description.

> (Copied from the original documentation.)

Ok. But this is not suited for a package description. Please create a better
description that is more serious, and explains what this prover can and cannot
do. Have a look at packages from similar software, like prover9, if you need
inspiration.

--
Met vriendelijke groet / with kind regards,
Guus Sliepen <guus@debian.org>
 
Old 02-23-2009, 06:13 AM
"Petr Pudlak (Debian)"
 
Default Bug#516545: ITP: eprover -- The Equational Theorem Prover E

Hi,



thanks for valuable comments. The original description was meant as a kind of mathematical joke, since the task of proving a theorem is in general undecidable, so any theorem prover will get stuck forever on many (or most) inputs. I didn't realize at first that tis would actually discourage potentials users.



Here is the corrected description:



* Package name * *: eprover

* Version * * * * : 1.0.004

* Upstream Author : Stephan Schulz <schulz@eprover.org>

* URL * * * * * * : http://www.eprover.org/

* License * * * * : GPL-2

* Programming Lang: C

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





Petr



On Sunday 22 February 2009 16:18:58 Guus Sliepen wrote:

> On Sun, Feb 22, 2009 at 09:57:04AM +0100, Petr Pudlak wrote:

> > * Package name : eprover

> > Description : The Equational Theorem Prover E

>

> That is not a description, that is just the name spelled out. A better

> description would be "equational theorem prover".

>

> > 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,

>

> So far so good...

>

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

>

> If I read this, I think: "What kind of crap software is this that suffers

> from infinite loops and only works for only a handful of equations? Why is

> it in Debian if there are other theorem provers that are apparently

> better?"

>

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

>

> That information belongs in the upstream NEWS or Changes file, not in a

> package description.

>

> > (Copied from the original documentation.)

>

> Ok. But this is not suited for a package description. Please create a

> better description that is more serious, and explains what this prover can

> and cannot do. Have a look at packages from similar software, like prover9,

> if you need inspiration.
 

Thread Tools




All times are GMT. The time now is 07:25 AM.

VBulletin, Copyright ©2000 - 2014, Jelsoft Enterprises Ltd.
Content Relevant URLs by vBSEO ©2007, Crawlability, Inc.
Copyright 2007 - 2008, www.linux-archive.org