
Isabelle/ZF
 Referenced in 63 articles
[sw04973]
 formalizes the greater part of elementary set theory, including relations, functions, injections, surjections, ordinals ... Wellordering Theorem. Isabelle/ZF also provides theories of lists, trees, etc., for formalizing computational notions ... cardinality of branching. (ZF: ZermeloFraenkel Set Theory...

IsarMathLib
 Referenced in 2 articles
[sw22729]
 logic which implements ZermeloFraenkel (untyped) set theory...

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

Isabelle
 Referenced in 698 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

ML
 Referenced in 522 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

Kenzo
 Referenced in 65 articles
[sw04861]
 The Kenzo program implements the general ideas of...

HOL
 Referenced in 583 articles
[sw05492]
 Higher Order Logic (HOL) is a programming environment...

Stata
 Referenced in 837 articles
[sw06029]
 Stata is a complete, integrated statistical package that...

Nuprl
 Referenced in 394 articles
[sw06751]
 The Nuprl system is a framework for reasoning...

Twelf
 Referenced in 171 articles
[sw06888]
 Twelf is a language used to specify, implement...

Automath
 Referenced in 410 articles
[sw07127]
 Automath is a language designed by N.G. the...

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

IMPS
 Referenced in 52 articles
[sw09143]
 IMPS: An interactive mathematical proof system. IMPS is...

LEGO
 Referenced in 107 articles
[sw09685]
 LEGO is an interactive proof development system (proof...

sprfn
 Referenced in 3 articles
[sw24048]
 Term rewriting: Some experimental results. We discuss term...