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.

More documentation about the competition may be found at

http://www.cs.jcu.edu.au/ftp/users/GSutcliffe/Competition.html