Proof assistant/External Links: Difference between revisions
Jump to navigation
Jump to search
imported>Boris Tsirelson (→Other projects: OMEGA) |
imported>Boris Tsirelson |
||
| Line 15: | Line 15: | ||
==Other projects== | ==Other projects== | ||
[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://imps.mcmaster.ca/ IMPS, An Interactive Mathematical Proof System] : [http://imps.mcmaster.ca/theories/theory-library.html Theory library] | |||
[http://pvs.csl.sri.com/ PVS Specification and Verification System] | [http://pvs.csl.sri.com/ PVS Specification and Verification System] | ||
[http://www.cse.chalmers.se/~hallgren/Alfa/ The Proof EditorAlpha] | [http://www.cse.chalmers.se/~hallgren/Alfa/ The Proof EditorAlpha] | ||
[http://www.risc.jku.at/research/theorema/software/ The Theorema System] | [http://www.risc.jku.at/research/theorema/software/ The Theorema System] | ||
[http://www.mathematik.uni-muenchen.de/~minlog/ MINLOG] | [http://www.mathematik.uni-muenchen.de/~minlog/ MINLOG] | ||
Revision as of 13:37, 14 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.
Isabelle/Isar
Isabelle : Overview, Download and installation, Projects, Theory library
IsarMathLib: A library of formalized mathematics for Isabelle/ZF
Other projects
Nuprl: Proof/Program Refinement Logic : Theory library
IMPS, An Interactive Mathematical Proof System : Theory library
PVS Specification and Verification System