Directory of Logical Frameworks Resources

Home > Science > Math > Logic and Foundations > Computational Logic > Logical Frameworks

A proof-assistant is a computer program with which a user can construct completely formal mathematical proofs in some kind of logical system. In contrast to a theorem prover, a proof-assistant cannot find proofs on its own

Subcategories

• Coq
• LF Logical Framework

Resources in This Category

• Af2 Proof Assistant

  http://www.lama.univ-savoie.fr/sitelama/Membres/pages_web/RAFFALLI/af2.html
  A type system based on second order intuitionistic logic.

• Alfa

  http://www.cs.chalmers.se/~hallgren/Alfa/
  A successor to the proof editor Alf with a graphical user interface, being developed at the Programming Logic Group at Chalmers. Available for download.

• Isabelle

  http://isabelle.informatik.tu-muenchen.de/
  Homepage of the theorem prover environment developed by Larry Paulson at Cambridge University and Tobias Kipkow at TU Munich.

• Kumo

  http://www.cs.ucsd.edu/groups/tatami/kumo/
  A web-based proof assistant. It assists with proofs in first order hidden logic, using OBJ3 as a reduction engine. The most important inference rules in first order logic and hidden equational logic are implemented, including induction and coinduction, generates proof documentation for the web, supports distributed cooperative proving.

• NuPrl Proof Development System

  http://www.cs.cornell.edu/Info/Projects/NuPrl/
  A powerful tactic-based proof assistant, developed over the last 15 years at Cornell University. Features include: very expressive logical language based on Martin-Lof type theory, extensive library of formal mathematics and automata theory, possibility of an extraction a certified program from the constructive proof of its formal specification, graphical proof editor. NuPrl was successfully used in verifying components of the Ensemble group communications system.

• Proof General

  http://zermelo.dcs.ed.ac.uk/~proofgen/
  Emacs based generic interface for theorem provers.

• The HOL Theorem Proving System

  http://hol.sourceforge.net/
  The system documented originated at the Laboratory for Applied Logic of Brigham Young University and features higher-order, classical, natural deduction with tactics.

• The LEGO Proof Assistant

  http://www.dcs.ed.ac.uk/home/lego/
  A powerful tool for interactive proof development in the natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes removing the more tedious aspects of interactive proofs.

• Yarrow

  http://www.cs.ru.nl/~janz/yarrow/
  A proof-assistant for Pure Type Systems (PTSs), representing different logics and programming languages. A basic knowledge of Pure Type Systems and the Curry-Howard-de Bruijn isomorphism is required. (This isomorphism says how you can interpret types as propositions.)

 

Home > Science > Math > Logic and Foundations > Computational Logic > Logical Frameworks

 

---

 

Thanks to DMOZ, which built a great web directory for nearly two decades and freely shared it with the web. About us