
OTTER
 Referenced in 310 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 169 articles
[sw04969]
 counterexamples. Prover9 is the successor of the Otter prover...

HR
 Referenced in 29 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 26 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 12 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...

Proofwatch
 Referenced in 3 articles
[sw28654]
 This mechanism has been used with the Otter and Prover9 theorem provers, both for interactive...

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

TDAstats
 Referenced in 1 article
[sw31276]
 persistent homology for topological data analysis, see Otter et al. (2017)

Maple
 Referenced in 4890 articles
[sw00545]
 The result of over 30 years of cutting...

SETHEO
 Referenced in 119 articles
[sw00707]
 SETHEO: A highperformance theorem prover. The paper...

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

VAMPIRE
 Referenced in 227 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem...

SPASS
 Referenced in 173 articles
[sw04108]
 SPASS is an automated theorem prover for first...