Proof assistant/External Links: Difference between revisions
Jump to navigation
Jump to search
imported>Boris Tsirelson |
imported>Meg Taylor No edit summary |
||
| (25 intermediate revisions by one other user not shown) | |||
| Line 1: | Line 1: | ||
{{subpages}} | {{subpages}} | ||
__NOTOC__ | |||
==Theorems== | |||
*[http://www.cs.ru.nl/~freek/100/ Formalizing 100 Theorems] | |||
[http://www. | *[http://www.cse.unsw.edu.au/~kleing/top100/#1 Top 100 theorems in Isabelle] | ||
[http://www. | ==Literature== | ||
Some books mentioned on the "Bibliography" page: | |||
*[http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf Nipkow, Paulson, Wenzel: Isabelle/HOL (tutorial)] (newer version, of 2010) | |||
*[http://www.cs.ru.nl/~freek/comparison/comparison.pdf The Seventeen Provers of the World] | |||
==Isabelle/Isar== | ==Isabelle/Isar== | ||
*[http://isabelle.in.tum.de/ Isabelle] : [http://isabelle.in.tum.de/overview.html Overview], | |||
*[http://isabelle.in.tum.de/documentation.html Documentation], | |||
*[http://isabelle.in.tum.de/download.html Download and installation], | |||
*[http://isabelle.in.tum.de/projects.html Projects], | |||
*[http://isabelle.in.tum.de/library/ Theory library], | |||
*[http://afp.sourceforge.net/ Journal] | |||
*[http://isarmathlib.org/ IsarMathLib: A library of formalized mathematics for Isabelle/ZF] : [http://www.nongnu.org/isarmathlib/ Questions and Answers] | |||
==Other projects== | |||
*[http://www.mizar.org/ Mizar] : [http://mizar.uwb.edu.pl/version/current/html/ Theory library] : [http://fm.mizar.org/ Journal] | |||
[http:// | *[http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html Nuprl: Proof/Program Refinement Logic] : [http://www.cs.cornell.edu/Info/Projects/NuPrl/Nuprl4.2/Libraries/Welcome.html Theory library] | ||
[http:// | |||
[http:// | *[http://imps.mcmaster.ca/ IMPS, An Interactive Mathematical Proof System] : [http://imps.mcmaster.ca/theories/theory-library.html Theory library] | ||
*[http://www.msr-inria.inria.fr/Projects/math-components Ssreflect] (Small Scale Reflection Extension for the Coq system) : [http://coqfinitgroup.gforge.inria.fr/ssreflect/ Theory library] | |||
*[http://coq.inria.fr/ Coq] : [http://coq.inria.fr/contribs/bycat.html Theory library] | |||
*[http://www.cl.cam.ac.uk/research/hvg/HOL/history.html HOL] (history and relatives) | |||
*[http://www.cl.cam.ac.uk/~jrh13/hol-light/ HOL Light] | |||
*[http://pvs.csl.sri.com/ PVS Specification and Verification System] | |||
*[http://www.cse.chalmers.se/~hallgren/Alfa/ The Proof EditorAlpha] | |||
[http://www. | *[http://www.risc.jku.at/research/theorema/software/ The Theorema System] | ||
[http:// | *[http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html PhoX] | ||
[http:// | *[http://jape.comlab.ox.ac.uk:8080/jape/ Jape] | ||
[http://www. | *[http://www.cs.unm.edu/~mccune/prover9/ Prover9] (and Mace4; successor of Otter). | ||
[http://www. | *[http://www.mathematik.uni-muenchen.de/~minlog/ MINLOG] | ||
[http://www. | *[http://www.ags.uni-sb.de/~omega/software/omega/ OMEGA] | ||
[http:// | *[http://matita.cs.unibo.it/ Matita] | ||
*[http://twelf.plparty.org/wiki/Main_Page Twelf] | |||
[http:// | *[http://us.metamath.org/index.html Metamath] | ||
[http:// | *[http://www.dcs.ed.ac.uk/home/lego/ Lego] (1999) | ||
[http:// | *[http://www-formal.stanford.edu/clt/ARS/ars-db.html Mechanized Reasoning] (1996) | ||
[http:// | *[http://www-formal.stanford.edu/clt/ARS/systems.html Database of Existing Mechanized Reasoning Systems] (1999) | ||
Latest revision as of 15:14, 3 November 2013
- Please sort and annotate in a user-friendly manner and consider archiving the URLs behind the links you provide. See also related web sources.
Theorems
Literature
Some books mentioned on the "Bibliography" page:
- Nipkow, Paulson, Wenzel: Isabelle/HOL (tutorial) (newer version, of 2010)
Isabelle/Isar
Other projects
- Ssreflect (Small Scale Reflection Extension for the Coq system) : Theory library
- HOL (history and relatives)
- Prover9 (and Mace4; successor of Otter).
- Lego (1999)
- Mechanized Reasoning (1996)