• QMLTP

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

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

  • Referenced in 6 articles [sw27551]
  • sequence models for premise selection in automated theorem proving, one of the main bottlenecks...
  • NQTHM

  • Referenced in 136 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...
  • LCF

  • Referenced in 144 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 5 articles [sw08574]
  • transformations, conics, parametric curves, flow control, automated theorem proving, etc. The basic idea behind GCLC...
  • dedukti

  • Referenced in 12 articles [sw13663]
  • Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning...
  • FOL Fitting

  • Referenced in 4 articles [sw28611]
  • book ”First-Order Logic and Automated Theorem Proving”. The formalization covers the syntax of first...
  • MPTP 0.2

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

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

  • Referenced in 10 articles [sw28307]
  • hypotheses and conclusions. Finally, automated theorem provers are used to prove the correctness...
  • Transfer

  • Referenced in 19 articles [sw21009]
  • build a library of operations and theorems about an abstract type, but they want ... Quotient package has yielded great progress in automation, but it still has many technical limitations ... packages: the Transfer package for proving theorems, and the Lifting package for defining constants ... more situations, and has more user-friendly automation...
  • Lifting

  • Referenced in 19 articles [sw21010]
  • build a library of operations and theorems about an abstract type, but they want ... Quotient package has yielded great progress in automation, but it still has many technical limitations ... packages: the Transfer package for proving theorems, and the Lifting package for defining constants ... more situations, and has more user-friendly automation...
  • SNARK

  • Referenced in 4 articles [sw19611]
  • Automated Reasoning Kit. SNARK is an automated theorem-proving program being developed in Common Lisp...
  • SymProve3

  • Referenced in 2 articles [sw09242]
  • difficult point in the field of automated theorem proving. In this paper, we provide...
  • DCTP

  • Referenced in 21 articles [sw06621]
  • Calculus Theorem Prover. DCTP is an automated theorem prover for first order clause logic. Given ... TPTP syntax, DCTP will attempt to prove either the unsatisfiability of the input formula...
  • Psyche

  • Referenced in 2 articles [sw28518]
  • engine designed for either interactive or automated theorem proving, and aiming at two things...
  • MMP/Geometer

  • Referenced in 13 articles [sw00584]
  • automate some of the basic geometric activities including geometric theorem proving, geometric theorem discovering ... only prove difficult geometric theorems but also discover new theorems and generate short and readable ... idea of dynamic geometry and methods of automated diagram generation...
  • CoCLAM

  • Referenced in 2 articles [sw28719]
  • present an automation of coinductive theorem proving. This automation is based on the idea ... focused on the use of coinduction to prove the equivalence of programs in a small ... been successfully tested on a number of theorems...
  • ToadsAndFrogs

  • Referenced in 3 articles [sw12648]
  • symbolic finite-state approach for automated proving of theorems in combinatorial game theory. We develop...