Running a competition for automated theorem Proving (ATP) systems is a difficult and arguable venture. However, the potential benefits of such an event by far outweigh the controversial aspects. The motivations for running the CADE-13 ATP system competition are to contribute to the evalaution of ATP systems, to simulate ATP research and system development, and to expose ATP systems to interested researchers both within and outside the ATP community. This paper identifies and discusses the issues that determine the nature of the competition. Choices and motivated decisions, with respect to the issues, are given.
展开▼
