
QMLTP
 Referenced in 7 articles
[sw09915]
 platform for testing and evaluating automated theorem proving (ATP) systems for firstorder 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, 117172 (1988)]. However...

LCF
 Referenced in 144 articles
[sw08360]
 whose in°uence on the ¯eld of automated reasoning has been diverse and profound ... invent the LCFapproach 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 ”FirstOrder 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 firstorder 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 userfriendly 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 userfriendly automation...

SNARK
 Referenced in 4 articles
[sw19611]
 Automated Reasoning Kit. SNARK is an automated theoremproving 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 finitestate approach for automated proving of theorems in combinatorial game theory. We develop...