• HR

  • Referenced in 29 articles [sw10392]
  • program for theorem generation. Automated theory formation involves the production of objects of interest, concepts ... only-if conjectures and these become theorems if they are proved, non-theorems 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 quantifier-free 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 first-order logic with equality ... equational programming system. Otter is a fourth-generation 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 first-order 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 boson-fermion 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 right-quantum matrix...
  • HipSpec

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

  • Referenced in 12 articles [sw21368]
  • KRHyper system is a model generator and theorem prover for first-order 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 model-generation 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...
  • I-SATCHMO

  • 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 Boyer-Moore...