• ML

  • Referenced in 522 articles [sw01218]
  • such as in compiler writing, automated theorem proving and formal verification. (wikipedia...
  • TPTP

  • Referenced in 395 articles [sw04143]
  • library of test problems for automated theorem proving (ATP) systems. The TPTP supplies...
  • HOL

  • Referenced in 588 articles [sw05492]
  • programming environment in which theorems can be proved and proof tools implemented. Built-in decision...
  • OTTER

  • Referenced in 316 articles [sw02904]
  • deduction system Otter is designed to prove theorems stated in first-order logic with equality...
  • ETPS

  • Referenced in 160 articles [sw06302]
  • ETPS are, respectively, the Theorem Proving System and the Educational Theorem Proving System. The former ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... under Windows. Potential applications of automated theorem proving include hardware and software verification, partial automation ... intelligence. TPS can be used to prove theorems of first- and higher-order logic interactively...
  • Isar

  • Referenced in 144 articles [sw04599]
  • Theorem proving system supporting both interactive proof development and some degree of automation have become ... state-of-the-art interactive theorem proving systems and an appropriate level of abstraction ... Isar/VM interpreter. Compared to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings ... into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc. may be used interchangeably...
  • SMT-LIB

  • Referenced in 196 articles [sw04103]
  • TPTP library has done for theorem proving, or the SATLIB library has done initially...
  • VAMPIRE

  • Referenced in 258 articles [sw02918]
  • result to the kernel. When a theorem is proved, the system produces a verifiable proof...
  • LCF

  • Referenced in 158 articles [sw08360]
  • invent the LCF-approach to theorem proving, but he also designed the ML programming language...
  • OBJ3

  • Referenced in 140 articles [sw05370]
  • software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among...
  • TPS

  • Referenced in 73 articles [sw00973]
  • ETPS are, respectively, the Theorem Proving System and the Educational Theorem Proving System. The former ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... under Windows. Potential applications of automated theorem proving include hardware and software verification, partial automation ... intelligence. TPS can be used to prove theorems of first- and higher-order logic interactively...
  • DGM

  • Referenced in 164 articles [sw39282]
  • basis functions. In addition, we prove a theorem regarding the approximation power of neural networks...
  • UNITY

  • Referenced in 185 articles [sw13461]
  • model should obey and prove them as theorems using the formal specification. The methodology...
  • MaLARea

  • Referenced in 48 articles [sw10278]
  • system works in cycles of theorem proving followed by machine learning from successful proofs, using ... available axioms for the next theorem proving cycle. Although the metasystem is quite simple...
  • MPTP 0.2

  • Referenced in 50 articles [sw02589]
  • version of the Mizar Problems for Theorem Proving (MPTP) system and first experimental results obtained ... available to current first-order automated theorem provers (ATPs) (and vice versa) and to boost ... already complete. About every fifth nonarithmetical theorem is proved in a fully autonomous mode...
  • Gandalf

  • Referenced in 35 articles [sw10133]
  • Gandalf is an automated theorem proving (ATP) system. It proves theorems formulated in logic. Since ... systems such as Gandalf can prove theorems in mathematics and verify complex systems such...
  • Abella

  • Referenced in 50 articles [sw09461]
  • Abella Interactive Theorem Prover (System Description). Abella [3] is an interactive system for reasoning about ... other things, Abella has been used to prove normalizability properties of the λ-calculus ... Abella, outlines the style of theorem proving that it supports and finally describes some...
  • Z/EVES

  • Referenced in 44 articles [sw10262]
  • specifications in CZT with theorem proving and verification capabilities. Z/EVES Eclipse provides a modern environment...
  • Lean

  • Referenced in 45 articles [sw15148]
  • between interactive and automated theorem proving, by situating automated tools and methods in a framework...
  • Daikon

  • Referenced in 44 articles [sw04319]
  • predicting incompatibilities in component integration, automating theorem proving, repairing inconsistent data structures, and checking...