
QMLTP
 Referenced in 8 articles
[sw09915]
 platform for testing and evaluating automated theorem proving (ATP) systems for firstorder modal logics...

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

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

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, 117172 (1988)]. However...

dedukti
 Referenced in 18 articles
[sw13663]
 Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning...

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

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

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

Psyche
 Referenced in 5 articles
[sw28518]
 engine designed for either interactive or automated theorem proving, and aiming at two things...

MPTP 0.2
 Referenced in 44 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...

FOL Fitting
 Referenced in 4 articles
[sw28611]
 book ”FirstOrder Logic and Automated Theorem Proving”. The formalization covers the syntax of first...

Transfer
 Referenced in 26 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 26 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...

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

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...

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...