The CADE 13 System Competition
David A. Plaisted
I wanted to report on the performance of provers of my students in the
CADE 13 System Competition. The provers entered by my students were
Violet, RRTP, CLIN-S, and CLIN-E. In the monolithic category,
E-SETHEO proved 36 theorems, OTTER with Wos' customized settings
proved 32, SETHEO proved 31, Violet proved 30, and RRTP proved 21.
One could say that Violet essentially tied for second place. Violet
had a better performance than Otter with the automatic flag set, which
was in another category and proved 28. In that category, SPASS was
the winner with 32. One can see that Violet is a first-class theorem
prover. Of course, Otter's strength is shown mainly in much longer
runs and in equality problems. Violet is a LISP prover written by my
student Steven Greenbaum at Illinois, and RRTP is a Prolog and C
prover written by M. Paramasivam at UNC. I believe that Violet was
the best LISP prover in its class and RRTP was the best (partially)
Prolog prover. It's interesting that in later runs, we obtained 24
proofs with the same time limit using RRTP. E-SETHEO is a highly
optimized model elimination prover written in something like a
specialized WAM code. OTTER is a resolution-paramodulation prover
written in C with efficient data structures. Setheo is like E-SETHEO
but without special equality methods. Violet uses resolution with
discrimination nets and something like Brand's modification method and
a priority structure to choose the best pair of clauses to resolve at
each step. RRTP reduces first-order logic to propositional calculus
and then applies an efficient propositional prover.
LINUS proved 25 in the same category. This is interesting because
this is a clause linking-based theorem prover written by Reinhold Letz
at Muenchen.
CLIN-S (9) and CLIN-E (4) proved many fewer theorems in another
category (special hardware). However, these provers generally require
longer time periods to obtain good performance, and also suffered from
running on slower machines. In addition, CLIN-S was designed to be
used with user-supplied semantics, but was run with a trivial
semantics. Finally, CLIN-E is only an initial implementation, and
does not have equality or all of the unit rules implemented yet.
More documentation about the competition may be found at
http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/Competition.html