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

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

OTTER
 Referenced in 204 articles
[sw02904]
 deduction system Otter is designed to prove theorems stated in firstorder logic with equality...

HOL
 Referenced in 291 articles
[sw05492]
 programming environment in which theorems can be proved and proof tools implemented. Builtin decision...

Isar
 Referenced in 92 articles
[sw04599]
 Theorem proving system supporting both interactive proof development and some degree of automation have become ... 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 ... into the Isabelle/Pure metalogic implementation. Theories, theorems, proof procedures etc. may be used interchangeably...

OBJ3
 Referenced in 121 articles
[sw05370]
 software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among...

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

LCF
 Referenced in 110 articles
[sw08360]
 invent the LCFapproach to theorem proving, but he also designed the ML programming language...

VAMPIRE
 Referenced in 151 articles
[sw02918]
 result to the kernel. When a theorem is proved, the system produces a verifiable proof...

SMTLIB
 Referenced in 93 articles
[sw04103]
 TPTP library has done for theorem proving, or the SATLIB library has done initially...

UNITY
 Referenced in 162 articles
[sw13461]
 model should obey and prove them as theorems using the formal specification. The methodology...

Z/EVES
 Referenced in 46 articles
[sw10262]
 specifications in CZT with theorem proving and verification capabilities. Z/EVES Eclipse provides a modern environment...

OMRS
 Referenced in 41 articles
[sw03359]
 communication of mathematical services in distributed theorem proving and symbolic computation environments...

Gandalf
 Referenced in 24 articles
[sw10133]
 Gandalf is an automated theorem proving (ATP) system. It proves theorems formulated in logic. Since ... systems such as Gandalf can prove theorems in mathematics and verify complex systems such...

MaLARea
 Referenced in 27 articles
[sw10278]
 system works in cycles of theorem proving followed by machine learning from successful proofs, using ... available axioms for the next theorem proving cycle. Although the metasystem is quite simple...

HR
 Referenced in 25 articles
[sw10392]
 these become theorems if they are proved, nontheorems if disproved. Similar to Zhang ... using the Otter theorem prover to prove conjectures. In domains where Otter and MACE ... effective, HR can produce large numbers of theorems for testing automated theorem provers (ATPs ... generation of lemmas for automated theorem proving, and the production of benchmark theorems...

GEOTHER 1.1
 Referenced in 27 articles
[sw02842]
 GEOTHER (GEOmetry THeorem provER), a module of Epsilon, is an environment implemented by Dongming Wang ... Java for manipulating and proving geometric theorems. In GEOTHER a theorem is specified by means ... needed in order to manipulate and prove the theorem. From the specification, GEOTHER can automatically ... dragging, and saved as PostScript files; prove the theorem using any of the five algebraic...

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

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

GEX
 Referenced in 25 articles
[sw09961]
 dynamic diagram drawing and automated geometry theorem proving and discovering. As a dynamic geometry software ... With these methods, users may automated prove geometry theorems, to discover new prrperties of theorems...