Proof assistant/External Links: Difference between revisions
imported>Boris Tsirelson (→Other projects: Mechanized Reasoning) |
imported>Boris Tsirelson |
||
| Line 25: | Line 25: | ||
==Other projects== | ==Other projects== | ||
[http://www.mizar.org/ Mizar] : [http://mizar.uwb.edu.pl/version/current/html/ Theory library] : [http://fm.mizar.org/ Journal] | [http://www.mizar.org/ Mizar] : [http://mizar.uwb.edu.pl/version/current/html/ Theory library] : [http://fm.mizar.org/ Journal] | ||
| Line 59: | Line 55: | ||
[http://www.ags.uni-sb.de/~omega/software/omega/ OMEGA] | [http://www.ags.uni-sb.de/~omega/software/omega/ OMEGA] | ||
[http://www-formal.stanford.edu/clt/ARS/ars-db.html Mechanized Reasoning] (1996) | |||
[http://www-formal.stanford.edu/clt/ARS/systems.html Database of Existing Mechanized Reasoning Systems] (1999) | |||
==Wikipedia== | ==Wikipedia== | ||
Revision as of 05:42, 18 August 2010
- Please sort and annotate in a user-friendly manner and consider archiving the URLs behind the links you provide. See also related web sources.
Literature
Some books mentioned on the "Bibliography" page:
Nipkow, Paulson, Wenzel: Isabelle/HOL (tutorial) (newer version, of 2010)
The Seventeen Provers of the World
Isabelle/Isar
Isabelle : Overview, Documentation, Download and installation, Projects, Theory library, Journal
IsarMathLib: A library of formalized mathematics for Isabelle/ZF : Questions and Answers
Other projects
Mizar : Theory library : Journal
Nuprl: Proof/Program Refinement Logic : Theory library
IMPS, An Interactive Mathematical Proof System : Theory library
Ssreflect (Small Scale Reflection Extension for the Coq system) : Theory library
HOL (history and relatives)
PVS Specification and Verification System
Prover9 (and Mace4; successor of Otter).
Mechanized Reasoning (1996)
Database of Existing Mechanized Reasoning Systems (1999)