[gentoo-science] sci-proof

[C Y]

--- Alexandre Buisse <nattfodd@g.o> wrote:

> Sign me up for sci-proof (even if it is only a subset of
> sci-mathematics). As far as I know, there is only coq, but I am
> working on adding agda, and we'll see from there...

I know of coq and otter in the "already present" category.  Candidates
for inclusion:

Isabelle (the devs don't see the need for a package - fair warning)
HOL http://hol.sourceforge.net/
Mizar (anybody know what the license is?) http://www.mizar.org
IMPS http://imps.mcmaster.ca/ (I think the license looks OK, but it 
     would probably need to be added to portage.)
nqthm http://www.computationallogic.com/software/nqthm/, maybe 
      http://www.computationallogic.com/software/pc-nqthm/ as well 
     (might be a bit dated now, but probably still worth including - 
      it's GPL)
ProofPower http://www.lemma-one.com/ProofPower/index/
PVS has a problematic license - it could be set up but I'm not sure
    if it's worthwhile.
NuPrl http://www.cs.cornell.edu/Info/Projects/NuPrl/ - this is another 
      one where I can't find the license, but it's an excellent 
      candidate for inclusion.
Larch might be of interest - http://www.sds.lcs.mit.edu/spd/larch/
MetaPRL http://metaprl.org/

Also interesting might be the Pcoq interface, although I don't know if
it is maintained any longer:  http://www-sop.inria.fr/lemme/pcoq/

I'm sure I missed a few.  Anyway, certainly enough to start :-).

Cheers,
CY

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com 
-- 
gentoo-science@g.o mailing list