• Roo

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

  • Referenced in 6 articles [sw09915]
  • platform for testing and evaluating automated theorem proving (ATP) systems for first-order modal logics...
  • 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 139 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...
  • DeepMath

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

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

  • Referenced in 10 articles [sw13663]
  • Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning...
  • MPTP 0.2

  • Referenced in 37 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...
  • 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...
  • 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...
  • ToadsAndFrogs

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

  • Referenced in 7 articles [sw08962]
  • symbolic execution and theorem proving. ConSIT is the first fully automated implementation of conditioned slicing...
  • Mella

  • Referenced in 1 article [sw09688]
  • Dependently typed programming based on automated theorem proving. Mella is a minimalistic dependently typed programming ... investigate the effective integration of automated theorem provers in this pure and simple setting. Such...
  • Moat

  • Referenced in 1 article [sw23080]
  • sound verification methodology (based on automated theorem proving and information flow analysis) for proving that...
  • Octopus

  • Referenced in 2 articles [sw10407]
  • search. This paper presents Octopus, an automated theorem-proving system that combines learning and parallel...