Proof assistant/External Links: Difference between revisions
Jump to navigation
Jump to search
imported>Boris Tsirelson (→Other projects: coq) |
imported>Boris Tsirelson m (→Other projects: coq) |
||
| Line 31: | Line 31: | ||
[http://imps.mcmaster.ca/ IMPS, An Interactive Mathematical Proof System] : [http://imps.mcmaster.ca/theories/theory-library.html Theory library] | [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://coq.inria.fr/ Coq] : [http://coq.inria.fr/contribs/bycat.html Theory library] | ||
[http://pvs.csl.sri.com/ PVS Specification and Verification System] | [http://pvs.csl.sri.com/ PVS Specification and Verification System] | ||
Revision as of 05:00, 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
PVS Specification and Verification System