The impact of CASC in the development of automated deduction systems: Guest-editorial
Robert Nieuwenhuis · AI Communications · 2002
The CADE Automated theorem proving System Competition (CASC) is held each year at the International Conference on Automated Deduction (CADE). The aim of CASC is to stimulate automated theorem proving (ATP) system development, and to expose ATP systems to interested researchers. CASC evaluates the performance of sound, fully automatic, firstorder ATP systems. The evaluation is in terms of the number of problems solved, proof objects built, and the average runtime for successful solutions, in the context of a bounded number of eligible problems chosen from the TPTP Problem Library [1], and a specified time limit for each solution attempt. It is widely accepted that the six CASCs held so far (since 1996) have been a catalyst for the impressive progress that has taken place since then in the development of the current high-performance provers. But it is sometimes also argued that CASC directs ATP research and implementation efforts towards certain issues (like finding heuristics or ‘tuning’ ATP systems for specific classes of TPTP problems or for the particular competition circumstances), this being to the detriment of other needed research. The purpose of this AICOM special issue on CASC has been to stimulate the discussion about the impact of CASC in the area, and to give organizers and participants an opportunity to publish their opinions, as well as the experimental results and design decisions of the different state-of-the-art systems that participate in CASC. This special issue is intended for all ATP researchers interested in CASC or similar events (participants, organizers, and others). Its call-for-paper stated that original articles were sought describing or discussing all aspects related to CASC-like competitions and provers. Solicited topics included: