• Kit

  • Referenced in 7 articles [sw22321]
  • problem is stated in the Boyer-Moore logic, and the proof is mechanically checked with...
  • Imandra

  • Referenced in 1 article [sw37911]
  • description). We describe Imandra, a modern computational logic theorem prover designed to bridge ... Boyer-Moore family like ACL2, and interactive proof assistants for typed higher-order logics. Imandra ... logic is computational, based on a pure subset of OCaml in which all functions ... waterfall and simplifier which ”lifts” many Boyer-Moore ideas to our typed higher-order setting...
  • ACL2

  • Referenced in 283 articles [sw00060]
  • ACL2 is both a programming language in which...
  • OMRS

  • Referenced in 39 articles [sw03359]
  • Communication protocols for mathematical services based on KQML...
  • Haskell

  • Referenced in 880 articles [sw03521]
  • Haskell is a standardized, general-purpose purely functional...
  • HOL

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

  • Referenced in 273 articles [sw06363]
  • OCaml is the most popular variant of the...
  • Nuprl

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

  • Referenced in 127 articles [sw07201]
  • Lisp (historically, LISP) is a family of computer...
  • NQTHM

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

  • Referenced in 11 articles [sw07734]
  • ACL2s: “the ACL2 sedan” ACL2 is the latest...
  • LCF

  • Referenced in 158 articles [sw08360]
  • Edinburgh LCF. A mechanized logic of computation. From...
  • UNITY

  • Referenced in 185 articles [sw13461]
  • Simulation model development and analysis in UNITY. We...
  • CLAM

  • Referenced in 41 articles [sw19619]
  • CLAM Proof Planner. OYSTER is an interactive proof...
  • Oyster

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