From COMP.LANG.ML Frequently Asked Questions and Answers (compiled by Dave Berry and Greg Morrisett) -------------------------------------------------------------------------- 7. Theorem Provers and ML (Collected by Paul Black, pblack@cs.berekeley.edu. Thanks Paul!) - LCF (Edinburgh LCF and Cambridge LCF) * written in the original Edinburgh dialect of ML from which SML developed. "Logic and Computation: Interactive Proof with Cambridge LCF" also by Lawrence C. Paulson. - Lego (LFCS, Edinburgh Univ., SML) * originally developed in CAML * latest version (5) now runs under SML/NJ * only higher-order resolution * available via anon. ftp from ftp.dcs.ed.ac.uk:/pub/lego - HOL90 Authors = Konrad Slind, Elsa Gunter elsa@research.att.com, slind@informatik.tu-muenchen.de http://lal.cs.byu.edu/lal/hol-documentation.html hol90 is a free implementation in SML/NJ of Mike Gordon's HOL logic (a polymorphic version of Church's Simple Type Theory). The system provides a lot of automated support including: - a powerful rewriting package; - pre-installed theories for booleans, products, sums, natural numbers, lists, and trees; - definition facilities for recursive types and recursive functions over those types (mutual recursion is also handled); - extensive libraries for strings, sets, group theory, integers, the real numbers, wellordered sets, automatic solution of goals involving linear arithmetic, tautology checking, inductively defined predicates, Hoare logic, Chandy and Misra's UNITY theory, infinite state automata, and many others. The HOL community has a lively mailing list accessible at info-hol-request@leopard.cs.byu.edu and a yearly user's meeting that alternates between Europe and North America. hol90 is available by anonymous ftp from machine = ftp.informatik.tu-muenchen.de directory = local/lehrstuhl/nipkow/hol90/hol90.6.tar.Z or machine = research.att.com directory = dist/ml/hol90/hol90.6.tar.Z - NuPrl (from Bob Constable`s group at Cornell) - Isabelle (Lawrence C. Paulson, Cambridge Univ. ) * has rewriting, but not many decision procedures. It does has things like model elimination-based decision procedures. * a generic automatic theorem prover i.e. you can program it to the logic system/proof system you want. Already has the following subsystems already implemented: i) FOL - first order logic ii) HOL - higher order logic iii) LCF - Logic of computable functions iv) LK - Gentzen system LK v) Modal - Modal logic systems T, S4, S43 vi) ZF - Zermelo-Fraenkel set theory * ftp from - MERILL (Brian Matthews, U. of Glasgow & Rutherford Appleton Laboratory) * written in standard ML * a general purpose order-sorted equational reasoning system * Allows the user to declare their own object language, allows AC-rewriting and AC-unification of terms and equations, has several completion algorithms, is built on a hierarchy of types known as Order-Sorting, and allows the user to try different termination methods. * available via anonymous ftp from the University of Glasgow, ftp address: ftp.dcs.glasgow.ac.uk (130.209.240.50) * Brian Matthews, brian@dcs.glasgow.ac.uk or bmm@inf.rl.ac.uk - FAUST (Karlsruhe) * a HOL add-on written in ML. * ftp from goethe.ira.uka.de (129.13.18.22) - Alf * written in SML * An implementation of Martin-Lofs type theory with dependent types * Proof editor * available by anonymous ftp from cs.chalmers.se * only higher-order resolution - Coq * written in Caml-Light (but Caml-Light and SML are VERY similar) * no serious automated reasoning subsystems (other than higher-order resolution), but has a VERY nice package for program verification. * available via anon. ftp from ftp.inria.fr:/INRIA/coq/V5.8 * possible contact: Chet Murthy - ICLHOL/ProofPower (ICL Secure Systems) * a commercial system using a reimplementation of HOL in SML * contact ProofPower-server@win.icl.co.uk - Lamdba/DIALOG (Abstract Hardware Ltd) * a commercial tool written in Poly/ML, neither of which is free. - Elf (Frank Pfenning, Carnegie Mellon Univ.) * Elf is a higher-order logic programming language based on the LF Logical Framework. * Elf is not a theorem prover per-se, but is useful for specifying and proving properties of programming languages, logics, and their implementations. A number of examples are provided with the distribution. * The Elf implementation is written in SML/NJ and should be easily portable to other SML implementations. * Elf can be ftp'd from alonzo.tip.cs.cmu.edu (128.2.209.194) in the directory /afs/cs/user/fp/public. * A bibliography and a collection of papers regarding LF and Elf can be found in the directory /afs/cs/user/fp/public/elf-papers. * There is an Elf mailing list. Contact elf-request@cs.cmu.edu to join. * For further information, contact Frank Pfenning (fp@cs.cmu.edu). References "ML for the Working Programmer" by Lawrence C. Paulson contains a small first-order theorem prover. Paulson also has a good chapter on writing theorem provers in ML in "Handbook of logic in computer science", Edited by: S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum. Oxford : Clarendon Press, 1992-. CALL#: QA76 .H2785 1992 Others We have an automated theorm proving system here at the University of Tasmania, but it is still under development, currently riddled with bugs and has an obscure "input language"; aside from those minor problems, it'd be perfect... La Monte H. Yarroll Edinburgh's Concurrency Workbench and Sussex's Process Algebra Mauipulator are also ML systems of note, though neither are interactive theorem provers. --------------------------------------------------------------------------