Proof assistant/External Links: Difference between revisions

From Citizendium
Jump to navigation Jump to search
imported>Boris Tsirelson
imported>Boris Tsirelson
Line 41: Line 41:


[http://www.risc.jku.at/research/theorema/software/ The Theorema System]
[http://www.risc.jku.at/research/theorema/software/ The Theorema System]
[http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html PhoX]


[http://jape.comlab.ox.ac.uk:8080/jape/ Jape]
[http://jape.comlab.ox.ac.uk:8080/jape/ Jape]

Revision as of 05:09, 18 August 2010

This article is developing and not approved.
 Main Article
 Discussion
Related Articles  [?]
Bibliography  [?]
External Links  [?]
Citable Version  [?]
 
https://en.citizendium.org/wiki/index.php?title=Proof_assistant/External_Links&printable=yes
A hand-picked, annotated list of Web resources about Proof assistant.
Please sort and annotate in a user-friendly manner and consider archiving the URLs behind the links you provide. See also related web sources.

Formalizing 100 Theorems

Top 100 theorems in Isabelle

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

Coq : Theory library

PVS Specification and Verification System

The Proof EditorAlpha

The Theorema System

PhoX

Jape

MINLOG

OMEGA

Wikipedia

WP:Interactive theorem proving

WP:Automated proof checking

WP:Isabelle (theorem prover)

WP:Fold (higher-order function)

Retrieved from "https://citizendium.org/wiki/index.php?title=Proof_assistant/External_Links&oldid=800905"