
MizarMode
 Referenced in 17 articles
[sw01973]
 concentration on simple and intuitive humanoriented proofs  have helped Mizar in developing and maintaining...

decNumber
 Referenced in 2 articles
[sw19031]
 requirements of commercial, financial, and humanoriented applications. It also matches the decimal arithmetic...

Coq
 Referenced in 1784 articles
[sw00161]
 Coq is a formal proof management system. It...

Theorema
 Referenced in 144 articles
[sw00961]
 The software system Theorema provides a uniform logic...

VAMPIRE
 Referenced in 237 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem...

NQTHM
 Referenced in 149 articles
[sw07543]
 A computational logic handbook. This book is a...

ForTheL
 Referenced in 8 articles
[sw09797]
 ForTheL — the language of formal theories. ForTheL, an...

Analytica
 Referenced in 31 articles
[sw10478]
 Analytica: A theorem prover for Mathematica. Analytica is...

Waldmeister
 Referenced in 44 articles
[sw19568]
 Waldmeister is a theorem prover for unit equational...

LambdaClam
 Referenced in 24 articles
[sw19614]
 LambdaClam ( λclam, lclam) is a proof planning system...

CLAM
 Referenced in 39 articles
[sw19619]
 CLAM Proof Planner. OYSTER is an interactive proof...

Oyster
 Referenced in 32 articles
[sw19629]
 Theorem proving and program synthesis with Oyster. Martin...

kepler98
 Referenced in 165 articles
[sw23625]
 The 1998 Proof of the Kepler Conjecture. The...

QuodLibet
 Referenced in 5 articles
[sw26306]
 QUODLIBET is an Inductive Theorem Proving (ITP) software...

Naproche
 Referenced in 10 articles
[sw28307]
 The Naproche project (Natural language Proof Checking) studies...

Cambridge LCF
 Referenced in 27 articles
[sw31981]
 Logic and computation. Interactive proof with Cambridge LCF...