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