Results 1 to 17 of 17
Sort by:

  • 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: Zermelo-Fraenkel Set Theory...

  • IsarMathLib
  • Referenced in 2 articles [sw22729]
  • logic which implements Zermelo-Fraenkel (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 general-purpose 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...

  • 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...