| Directory > Science > Math > Logic and Foundations > Computational Logic > Logical Frameworks The HOL Theorem Proving System
The system documented originated at the Laboratory for Applied Logic of Brigham Young University
and features higher-order, classical, natural deduction with tactics.
http://hol.sourceforge.net/
Reviews Rating: Not yet Rated
Whois Check
The Practice of Logical Frameworks
Comprehensive survey article by Frank Pfenning (1996) discussing the history of work on logical
frameworks and their current open problems.
http://citeseer.nj.nec.com/pfenning96practice.html
Reviews Rating: Not yet Rated
Whois Check
Isabelle
Homepage of the theorem prover environment developed by Larry Paulson at Cambridge University and
Tobias Kipkow at TU Munich.
http://isabelle.informatik.tu-muenchen.de/
Reviews Rating: Not yet Rated
Whois Check
Af2 Proof Assistant
A type system based on second order intuitionistic logic.
http://www.lama.univ-savoie.fr/sitelama/Membres/pages_web//RAFFALLI/af2.html
Reviews Rating: Not yet Rated
Whois Check
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.)
http://www.cs.kun.nl/~janz/yarrow/
Reviews Rating: Not yet Rated
Whois Check
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.
http://www.cs.ucsd.edu/groups/tatami/kumo/
Reviews Rating: Not yet Rated
Whois Check
Proof General
Emacs based generic interface for theorem provers.
http://zermelo.dcs.ed.ac.uk/~proofgen/
Reviews Rating: Not yet Rated
Whois Check
NuPrl Proof Development System
A powerful tactic-based proof assistant, developed over the last 15 years at Cornell University.
IFeatures 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.
http://www.cs.cornell.edu/Info/Projects/NuPrl/
Reviews Rating: Not yet Rated
Whois Check
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.
http://www.cs.chalmers.se/~hallgren/Alfa/
Reviews Rating: Not yet Rated
Whois Check
The LEGO Proof Assistant
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.
http://www.dcs.ed.ac.uk/home/lego/
Reviews Rating: Not yet Rated
Whois Check
MetaPRL logical programming environment
The next generation of the NuPrl proof development system. The main new features of MetaPRL
include: 1) Modularity. Programs and logics are developed as modules that define computational,
heuristic, and mathematical properties. 2) Speed. MetaPRL is more than two orders of magnitude
faster than NuPrl.
http://cvs.metaprl.org:12000/metaprl/
Reviews Rating: Not yet Rated
Whois Check
|
