
OTTER
 Referenced in 290 articles
[sw02904]
 current automated deduction system Otter is designed to prove theorems stated in firstorder 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 fourthgeneration 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 nearlinear 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]
 theoremproving 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...

OTT2MIZ
 Referenced in 1 article
[sw21546]
 ott2miz  otter to Mizar translator...

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 highperformance theorem prover. The paper...

MACSYMA
 Referenced in 690 articles
[sw01209]
 Macsyma is a general purpose symbolicnumericalgraphical...

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...