• TPTP

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

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

  • Referenced in 62 articles [sw00973]
  • Educational Theorem Proving System. The former is an automated theorem-prover for first-order logic ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... extent under Windows. Potential applications of automated theorem proving include hardware and software verification, partial ... intelligence. TPS can be used to prove theorems of first- and higher-order logic interactively...
  • OTTER

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

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

  • Referenced in 25 articles [sw10392]
  • program for theorem generation. Automated theory formation involves the production of objects of interest, concepts ... conjectures and these become theorems if they are proved, non-theorems if disproved. Similar ... produce large numbers of theorems for testing automated theorem provers (ATPs), or smaller numbers ... problems, the generation of lemmas for automated theorem proving, and the production of benchmark theorems...
  • Isar

  • Referenced in 91 articles [sw04599]
  • Theorem proving system supporting both interactive proof development and some degree of automation have become ... Typical examples of this kind of semi-automated reasoning systems include ... 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...
  • Gandalf

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

  • Referenced in 23 articles [sw09961]
  • dynamic diagram drawing and automated geometry theorem proving and discovering. As a dynamic geometry software ... learning of various mathematical concepts. As an automated reasoning software, we can build dynamic logic ... With these methods, users may automated prove geometry theorems, to discover new prrperties of theorems...
  • Ivy

  • Referenced in 21 articles [sw10279]
  • proved. The application is resolution/paramodulation automated theorem proving for first-order logic. The top ACL2...
  • ILTP

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

  • Referenced in 7 articles [sw06823]
  • Automated theorem proving for software analysis Automated theorem provers (ATPs) are a key component that...
  • TGTP

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

  • Referenced in 7 articles [sw12478]
  • paper we describe the application to automated theorem proving, which can be viewed...
  • MPTP

  • Referenced in 15 articles [sw02489]
  • theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system for translating the Mizar ... format suitable for automated theorem provers, and for generating theorem proving problems corresponding...
  • EQP

  • Referenced in 5 articles [sw15620]
  • Equational Prover. EQP is an automated theorem proving program for first-order equational logic...
  • LCF

  • Referenced in 110 articles [sw08360]
  • 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...
  • WinGCLC

  • Referenced in 4 articles [sw08574]
  • transformations, conics, parametric curves, flow control, automated theorem proving, etc. The basic idea behind GCLC...
  • NQTHM

  • Referenced in 91 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...
  • ASASP

  • Referenced in 3 articles [sw06350]
  • Satisfiability Modulo Theories solving and Automated Theorem Proving. asasp has been successfully applied...