Proof assistant/External Links: Difference between revisions

From Citizendium
Jump to navigation Jump to search
imported>Boris Tsirelson
imported>Meg Taylor
No edit summary
 
(20 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.cs.ru.nl/~freek/100/ Formalizing 100 Theorems]
*[http://www.cse.unsw.edu.au/~kleing/top100/#1 Top 100 theorems in Isabelle]
 
[http://www.cse.unsw.edu.au/~kleing/top100/#1 Top 100 theorems in Isabelle]


==Literature==
==Literature==
Some books mentioned on the "Bibliography" page:
Some books mentioned on the "Bibliography" page:


[http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf Nipkow, Paulson, Wenzel: Isabelle/HOL (tutorial)]
*[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]
*[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://isabelle.in.tum.de/ Isabelle] : [http://isabelle.in.tum.de/overview.html Overview],
*[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://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://isarmathlib.org/ IsarMathLib: A library of formalized mathematics for Isabelle/ZF] : [http://www.nongnu.org/isarmathlib/ Questions and Answers]
*[http://imps.mcmaster.ca/ IMPS, An Interactive Mathematical Proof System] : [http://imps.mcmaster.ca/theories/theory-library.html Theory library]


==Other projects==
*[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.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://www.risc.jku.at/research/theorema/software/ The Theorema System]


[http://imps.mcmaster.ca/ IMPS, An Interactive Mathematical Proof System] : [http://imps.mcmaster.ca/theories/theory-library.html Theory library]
*[http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html PhoX]


[http://pvs.csl.sri.com/ PVS Specification and Verification System]
*[http://jape.comlab.ox.ac.uk:8080/jape/ Jape]


[http://www.cse.chalmers.se/~hallgren/Alfa/ The Proof EditorAlpha]
*[http://www.cs.unm.edu/~mccune/prover9/ Prover9] (and Mace4; successor of Otter).


[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]
*[http://www.ags.uni-sb.de/~omega/software/omega/ OMEGA]


[http://www.ags.uni-sb.de/~omega/software/omega/ OMEGA]
*[http://matita.cs.unibo.it/ Matita]


==Wikipedia==
*[http://twelf.plparty.org/wiki/Main_Page Twelf]


[http://en.wikipedia.org/wiki/Interactive_theorem_proving WP:Interactive theorem proving]
*[http://us.metamath.org/index.html Metamath]


[http://en.wikipedia.org/wiki/Automated_proof_checking WP:Automated proof checking]
*[http://www.dcs.ed.ac.uk/home/lego/ Lego] (1999)


[http://en.wikipedia.org/wiki/Isabelle_(theorem_prover) WP:Isabelle (theorem prover)]
*[http://www-formal.stanford.edu/clt/ARS/ars-db.html Mechanized Reasoning] (1996)


[http://en.wikipedia.org/wiki/Fold_(higher-order_function) WP:Fold (higher-order function)]
*[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

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.

Theorems

Literature

Some books mentioned on the "Bibliography" page:

Isabelle/Isar

Other projects

  • HOL (history and relatives)
  • Prover9 (and Mace4; successor of Otter).
Retrieved from "https://citizendium.org/wiki/index.php?title=Proof_assistant/External_Links&oldid=746363"