Results of the CADE-13 ATP System Competition.pdf

ASSOCIATION FOR AUTOMATED REASONING NEWSLETTER No. 34 October 1996 From the AAR President, Larry Wos... Maiora meliora. This issue is certainly both|bigger and better. Of especial interest are two articles on the use of automated theorem provers (IPR and ILF) and one article on Godels algo- rithm for class formation. This mix of theory, application, and implementation is most pleasing. I am also delighted to invite AAR members|and anyone else who wishes to use the (perhaps) rst-ever completely push-button theorem prover|to check out Son of Bird Brain at http://www. /home/mccune/ar/sobb/. It lets the user construct some simple conjectures and run them through Otter (for proofs) and MACE (for models and counterexamples), two of Argonnes automated deduction systems|all within a few seconds. Its designed to hook the tyro|and I think it will! Results of the CADE-13 ATP System Competition Geo Sutclie James Cook University, Australia geo@.au The CADE-13 ATP System Competition was held on August 1, 1996, at CADE-13. The competition had several categories, according to the hardware, problems, and ATP system type. In the General Hardware categories, where all the systems used the same hardware, the fol- lowing systems were the winners:  Mixed problems - Monolithic systems: E-SETHEO, entered by Reinhold Letz from TU Munchen  Mixed problems - Compositional systems: SPASS, entered by Christoph Weidenbach from MPI Saarbruecken  Unit equality problems: Otter 3.0.4z, entered by William McCune from Argonne National Laboratory In the Special Hardware categories, no winners were announced because of the large dierences between the hardware used. Details of the results are now available through the competition Web page: 1 rmatik.tu-muenchen.de/~suttner/Competition.html In addition, a full archive of the competition is available, including entrants binaries; the sound- ness testing problems and output les; the eligible problem les, precisely as used in the compe- tition; an