
HR
 Referenced in 29 articles
[sw10392]
 program for theorem generation. Automated theory formation involves the production of objects of interest, concepts ... onlyif conjectures and these become theorems if they are proved, nontheorems if disproved ... works by (i) using the MACE model generator to generate objects of interest from axiom ... constraint satisfaction problems, the generation of lemmas for automated theorem proving, and the production...

UNITY
 Referenced in 184 articles
[sw13461]
 them as theorems using the formal specification. The methodology is illustrated through generation...

MPTP
 Referenced in 23 articles
[sw02489]
 automated theorem provers, and for generating theorem proving problems corresponding to MML. The first version ... generates about 30000 problems from complete proofs of Mizar theorems, and about 630000 problems from...

GEX
 Referenced in 35 articles
[sw09961]
 discover new prrperties of theorems, and to generate readable proofs for mant geometry throerms...

SATCHMO
 Referenced in 96 articles
[sw06619]
 SATCHMO Theorem Prover was one of the first systems which used model generation...

STP
 Referenced in 41 articles
[sw34795]
 Simple Theorem Prover. STP is a constraint solver for the theory of quantifierfree bitvectors ... many kinds of problems generated by program analysis tools, theorem provers, automated bug finders, cryptographic...

MMP/Geometer
 Referenced in 13 articles
[sw00584]
 theorem discovering, and geometric diagram generation. As a theorem prover, MMP/Geometer implements Wu’s method ... geometric theorems but also discover new theorems and generate short and readable proofs...

OTTER
 Referenced in 314 articles
[sw02904]
 deduction system Otter is designed to prove theorems stated in firstorder logic with equality ... equational programming system. Otter is a fourthgeneration Argonne National Laboratory deduction system whose ancestors...

GEOTHER 1.1
 Referenced in 31 articles
[sw02842]
 prove the theorem using any of the five algebraic provers; translate the generated algebraic nondegeneracy ... geometric/predicate form; generate an HTML, LaTeX, and/or PostScript file documenting the theorem and its proof...

MGTP
 Referenced in 7 articles
[sw09701]
 model generation based theorem prover MGTP for firstorder logic. This paper describes the major ... research and development of a model generation theorem prover MGTP. It exploits OR parallelism ... Horn magic set to suppress the generation of useless model candidates caused by irrelevant clauses...

QuantumMACMAHON
 Referenced in 19 articles
[sw11441]
 Zeilberger: The MacMahon’s Master Theorem relates a certain generating function obtained from a square ... equivalent formulation of this theorem is the bosonfermion correspondence in physics. In order ... quantum version of the MacMahon’s Master Theorem, the authors considered the quantum determinant ... obtained in this paper relates a certain generating function obtained from a rightquantum matrix...

HipSpec
 Referenced in 14 articles
[sw07736]
 exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems...

EKRHyper
 Referenced in 12 articles
[sw21368]
 KRHyper system is a model generator and theorem prover for firstorder logic with equality...

Daikon
 Referenced in 43 articles
[sw04319]
 used for generating test cases, predicting incompatibilities in component integration, automating theorem proving, repairing inconsistent...

SATCHMOREBID
 Referenced in 7 articles
[sw06623]
 integrate relevancy testing with the modelgeneration theorem prover SATCHMO. This made it possible...

BRAID
 Referenced in 18 articles
[sw04311]
 group. By Riemann’s existence theorem, braid orbits of generating systems for G with product...

CLT
 Referenced in 6 articles
[sw11432]
 Doron Zeilberger. ”The automatic central limit theorems generator (and much more...

ISATCHMO
 Referenced in 6 articles
[sw06622]
 other refinements, and effective for model generation theorem proving...

Electronic Geometry Textbook
 Referenced in 8 articles
[sw08745]
 relations among those data, for automatically generating readable documents for viewing or printing ... resulting textbook. By integrating an external geometric theorem prover and an external dynamic geometry software ... offers the facilities for automatically proving theorems and generating dynamic figures in the created textbooks...

PREVAIL
 Referenced in 7 articles
[sw02114]
 defined templates, and a theorem is generated in a form acceptable by the BoyerMoore...