--- Alexandre Buisse <[EMAIL PROTECTED]> 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 -- [email protected] mailing list
