Evaluating Automated Theorem Proving Systems

Introduction

• ATP, What is it?, What is it good for?, What Systems are Successful?
• Evaluation, What's it like?, What is Required?
• Aims for evaluating ATP systems, ATP problems

A Basis for Evaluation

• The TPTP Problem Library
• The SZS Ontology
• The TSTP Solution Library

Evaluating Systems and Problems

• Systems and Problems and Data
• Ranking and Rating
• Resource Usage

The CADE ATP System Competition

• History and Organization
• Systems, Problems, and Ranking
• Divisions and Entry Rules
• Results
• Pros and Cons and Great T-shirts