
TPTP
 Referenced in 272 articles
[sw04143]
 library of test problems for automated theorem proving (ATP) systems. The TPTP supplies...

ETPS
 Referenced in 134 articles
[sw06302]
 Educational Theorem Proving System. The former is an automated theoremprover for firstorder logic ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... extent under Windows. Potential applications of automated theorem proving include hardware and software verification, partial ... intelligence. TPS can be used to prove theorems of first and higherorder logic interactively...

TPS
 Referenced in 66 articles
[sw00973]
 Educational Theorem Proving System. The former is an automated theoremprover for firstorder logic ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... extent under Windows. Potential applications of automated theorem proving include hardware and software verification, partial ... intelligence. TPS can be used to prove theorems of first and higherorder logic interactively...

OTTER
 Referenced in 236 articles
[sw02904]
 current automated deduction system Otter is designed to prove theorems stated in firstorder logic...

Daikon
 Referenced in 34 articles
[sw04319]
 cases, predicting incompatibilities in component integration, automating theorem proving, repairing inconsistent data structures, and checking...

Isar
 Referenced in 107 articles
[sw04599]
 Theorem proving system supporting both interactive proof development and some degree of automation have become ... Typical examples of this kind of semiautomated reasoning systems include ... stateoftheart interactive theorem proving systems and an appropriate level of abstraction ... Isar/VM interpreter. Compared to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings...

Ivy
 Referenced in 26 articles
[sw10279]
 proved. The application is resolution/paramodulation automated theorem proving for firstorder logic. The top ACL2...

Gandalf
 Referenced in 28 articles
[sw10133]
 Gandalf is an automated theorem proving (ATP) system. It proves theorems formulated in logic. Since...

HR
 Referenced in 25 articles
[sw10392]
 program for theorem generation. Automated theory formation involves the production of objects of interest, concepts ... conjectures and these become theorems if they are proved, nontheorems if disproved. Similar ... produce large numbers of theorems for testing automated theorem provers (ATPs), or smaller numbers ... problems, the generation of lemmas for automated theorem proving, and the production of benchmark theorems...

GEX
 Referenced in 25 articles
[sw09961]
 dynamic diagram drawing and automated geometry theorem proving and discovering. As a dynamic geometry software ... learning of various mathematical concepts. As an automated reasoning software, we can build dynamic logic ... With these methods, users may automated prove geometry theorems, to discover new prrperties of theorems...

ILTP
 Referenced in 18 articles
[sw00437]
 platform for testing and benchmarking automated theorem proving (ATP) systems for firstorder and propositional...

Lean
 Referenced in 9 articles
[sw15148]
 bridge the gap between interactive and automated theorem proving, by situating automated tools and methods...

Zap
 Referenced in 7 articles
[sw06823]
 Automated theorem proving for software analysis Automated theorem provers (ATPs) are a key component that...

TGTP
 Referenced in 8 articles
[sw12327]
 testing and evaluation of geometric automated theorem proving (GATP) systems, to help ensure that performance...

MPTP
 Referenced in 18 articles
[sw02489]
 theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system for translating the Mizar ... format suitable for automated theorem provers, and for generating theorem proving problems corresponding...

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

OmegaANTS
 Referenced in 7 articles
[sw19626]
 open approach at combining interactive and automated theorem proving. We present the $Omega$ANTS theorem...

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

HERBY
 Referenced in 3 articles
[sw21545]
 Automated theorem proving. Theory and practice. With CDROM. The subject of this book ... most interesting area in Artificial Intelligence: automated theorem proving. In particular, it is about ... chapter, 13, briefly examines two other automated theoremproving programs, {it Gandalf} and {it Otter ... hundred theorems, can serve as instructional material for a course on theorem proving...

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