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

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

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

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

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 finitestate 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 theoremproving system that combines learning and parallel...