Vampire
Code
http://vprover.org/
Vampire is a theorem prover that is a system able to prove theorems. More precisely, it proves theor...
596 views
 
http://www.cs.cmu.edu/afs/cs/project/airepository/ai/areas/reasonng/atp/systems/frapps/0.html
FRAPPS (Framework for Resolutionbased Automated Proof Procedures) is a portable resolution theorem...
1690 views
 
NASA PVS Library
Code
ftp/larc/PVSlibrary/
The NASA PVS Library is a collection of formal developments in PVS maintained by the NASA Langley Fo...
1851 views
 
http://pvs.csl.sri.com/
PVS is a verification system: that is, a specification language integrated with support tools and a ...
833 views
 
HOL4
Code
http://hol.sourceforge.net/
HOL4 is the latest version of the HOL interactive proof assistant for higher order logic: a programm...
1637 views
 
CVC3
Code
http://www.cs.nyu.edu/acsys/cvc3/
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be use...
1930 views
 
CVC4
Code
https://github.com/CVC4/CVC4
CVC4 is an efficient opensource automatic theorem prover for satisfiability modulo theories (SMT) p...
1640 views
 
http://verify.stanford.edu/SVC/
The Stanford Validity Checker (SVC for short) is a research tool to check the validity of formulas e...
750 views
 
Princess
Code
http://www.philipp.ruemmer.org/princess.shtml
Princess is a theorem prover for Presburger arithmetic with uninterpreted predicates.
824 views
