• TPTP

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

  • Referenced in 153 articles [sw06302]
  • Educational Theorem Proving System. The former is an automated theorem-prover for first-order logic ... students; it contains only commands relevant to proving theorems interactively. TPS and ETPS ... Linux systems, and to some extent under Windows. Potential applications of automated theorem proving include ... disciplines, deductive information systems for these disciplines, expert systems which can reason, and certain aspects...
  • OTTER

  • Referenced in 313 articles [sw02904]
  • current automated deduction system Otter is designed to prove theorems stated in first-order logic...
  • TPS

  • Referenced in 71 articles [sw00973]
  • Educational Theorem Proving System. The former is an automated theorem-prover for first-order logic ... students; it contains only commands relevant to proving theorems interactively. TPS and ETPS ... Linux systems, and to some extent under Windows. Potential applications of automated theorem proving include ... disciplines, deductive information systems for these disciplines, expert systems which can reason, and certain aspects...
  • Isar

  • Referenced in 140 articles [sw04599]
  • Theorem proving system supporting both interactive proof development and some degree of automation have become ... none of the existing semi-automated reasoning systems have an adequate primary notion of proof ... state-of-the-art interactive theorem proving systems and an appropriate level of abstraction ... interpreter. Compared to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings...
  • ML

  • Referenced in 514 articles [sw01218]
  • polymorphic Hindley–Milner type system, which automatically assigns the types of most expressions without requiring ... languages, such as in compiler writing, automated theorem proving and formal verification. (wikipedia...
  • Gandalf

  • Referenced in 34 articles [sw10133]
  • Gandalf is an automated theorem proving (ATP) system. It proves theorems formulated in logic. Since...
  • ILTP

  • Referenced in 26 articles [sw00437]
  • platform for testing and benchmarking automated theorem proving (ATP) systems for first-order and propositional...
  • LCF

  • Referenced in 157 articles [sw08360]
  • short history. The original LCF system was a proof-checking program developed at Stanford University ... whose in°uence on the ¯eld of automated reasoning has been diverse and profound ... invent the LCF-approach to theorem proving, but he also designed the ML programming language ... underlying it and the innovative polymorphic type system used both...
  • HR

  • Referenced in 29 articles [sw10392]
  • program for theorem generation. Automated theory formation involves the production of objects of interest, concepts ... proved, non-theorems if disproved. Similar to Zhang’s MCS program, the HR system -- named ... using the Otter theorem prover to prove conjectures. In domains where Otter and MACE ... problems, the generation of lemmas for automated theorem proving, and the production of benchmark theorems...
  • TGTP

  • Referenced in 10 articles [sw12327]
  • testing and evaluation of geometric automated theorem proving (GATP) systems, to help ensure that performance...
  • NQTHM

  • Referenced in 149 articles [sw07543]
  • logic were described completely in their “Metafunctions: proving them correct and using them efficiently ... computational logic and its theorem prover” [J. Autom. Reasoning 4, No.2, 117-172 (1988)]. However ... authors’ former book, while the system has been applied to more and more difficult problems...
  • PROMELA

  • Referenced in 30 articles [sw07635]
  • specification language for modeling interactions in distributed systems, and for expressing logical correctness requirements about ... produce automated proofs for each type of property. SPIN either proves that a property ... valid in the given system, or it generates a counterexample that shows that...
  • MPTP

  • Referenced in 23 articles [sw02489]
  • MPTP (Mizar Problems for Theorem Proving) is a system for translating the Mizar Mathematical Library ... format suitable for automated theorem provers, and for generating theorem proving problems corresponding ... describe the design and structure of the system, the main problems encountered in this kind...
  • QMLTP

  • Referenced in 8 articles [sw09915]
  • platform for testing and evaluating automated theorem proving (ATP) systems for first-order modal logics...
  • TPA

  • Referenced in 13 articles [sw10114]
  • tool for proving termination of term rewrite systems (TRSs) in a fully automated fashion...
  • Daikon

  • Referenced in 43 articles [sw04319]
  • Daikon system for dynamic detection of likely invariants. Daikon is an implementation of dynamic detection ... cases, predicting incompatibilities in component integration, automating theorem proving, repairing inconsistent data structures, and checking...
  • MPTP 0.2

  • Referenced in 44 articles [sw02589]
  • Mizar Problems for Theorem Proving (MPTP) system and first experimental results obtained with ... Library (MML) available to current first-order automated theorem provers (ATPs) (and vice versa ... Mizar schemes are now handled by the system, too, by remembering (and, if necessary, abstracting ... longer detected by the ATP systems, suggesting that the `Mizar deconstruction’ done by MPTP...
  • HipSpec

  • Referenced in 13 articles [sw07736]
  • Automating inductive proofs using theory exploration HipSpec is a system for automatically deriving and proving...
  • Lean

  • Referenced in 30 articles [sw15148]
  • Lean theorem prover (system description). Lean is a new open source theorem prover being developed ... bridge the gap between interactive and automated theorem proving, by situating automated tools and methods ... used to embed it into other systems. It is currently being used to formalize category...