• OTTER

  • Referenced in 290 articles [sw02904]
  • current automated deduction system Otter is designed to prove theorems stated in first-order logic ... with equality. Otter’s inference rules are based on resolution and paramodulation, and it includes ... directing and restricting searches for proofs. Otter can also be used as a symbolic calculator ... embedded equational programming system. Otter is a fourth-generation Argonne National Laboratory deduction system whose...
  • Prover9

  • Referenced in 147 articles [sw04969]
  • counterexamples. Prover9 is the successor of the Otter prover...
  • HR

  • Referenced in 27 articles [sw10392]
  • conjecture making itself and (iii) using the Otter theorem prover to prove conjectures. In domains ... where Otter and MACE are effective, HR can produce large numbers of theorems for testing...
  • SCOTT

  • Referenced in 25 articles [sw06717]
  • SCOTT: Semantically Constrained Otter. The SCOTT project dates back to 1991 and is still running ... theorem prover, a variant of OTTER, has competed in CASC for several years, achieving unspectacular...
  • EQP

  • Referenced in 11 articles [sw15620]
  • polished as our main production theorem prover Otter. But it has obtained several interesting results ... good, but if you already know Otter, you might not have great difficulty in learning...
  • Bliksem

  • Referenced in 15 articles [sw21346]
  • which are used in E, Spass and Otter) can sometimes be dramatically slower...
  • Roo

  • Referenced in 7 articles [sw12478]
  • have applied the parallel closure algorithm to OTTER, currently the fastest sequential theorem proving system ... large problems. The result is ROO (Radical Otter Optimization, with Australian origins), a parallel theorem ... prover compatible with OTTER and capable of near-linear speedup over OTTER on shared memory...
  • Aquarius

  • Referenced in 5 articles [sw26678]
  • method. Aquarius incorporates the sequential theorem prover Otter, in such a way that Aquarius implements ... methodology, of all the strategies provided in Otter. In this paper, we give first...
  • HERBY

  • Referenced in 6 articles [sw21545]
  • theorem-proving programs, {it Gandalf} and {it Otter}. par In his past, the author...
  • SNARK

  • Referenced in 4 articles [sw19611]
  • style of theorem proving is similar to Otter’s. Some distinctive features of SNARK...
  • GLEFatinf

  • Referenced in 2 articles [sw26321]
  • system. In particular, we present an OTTER [McC90] proof in which we handle symmetries...
  • PTTP+GLiDeS

  • Referenced in 2 articles [sw30126]
  • proving paradigms: SCOTT [8] is based on OTTER and is a forward chaining resolution system...
  • Proofwatch

  • Referenced in 1 article [sw28654]
  • This mechanism has been used with the Otter and Prover9 theorem provers, both for interactive...
  • Maple

  • Referenced in 4699 articles [sw00545]
  • The result of over 30 years of cutting...
  • SETHEO

  • Referenced in 114 articles [sw00707]
  • SETHEO: A high-performance theorem prover. The paper...
  • MACSYMA

  • Referenced in 690 articles [sw01209]
  • Macsyma is a general purpose symbolic-numerical-graphical...
  • VAMPIRE

  • Referenced in 203 articles [sw02918]
  • Vampire 8.0, [RV02,Vor05] is an automatic theorem...
  • SPASS

  • Referenced in 154 articles [sw04108]
  • SPASS is an automated theorem prover for first...
  • TPTP

  • Referenced in 333 articles [sw04143]
  • The TPTP (Thousands of Problems for Theorem Provers...