The CADE ATP System Competition

The World Championship for Automated Theorem Proving

(Not The Coalition for Academic Scientific Computation)


The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC evaluates the performance of sound, fully automatic, classical logic ATP systems. CASC evaluates the performance of sound, fully automatic, classical logic order ATP systems. The evaluation is in terms of:

in the context of:

The competition organizers are Geoff Sutcliffe and Christian Suttner. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. If you have any questions about the competition, please email the organizers.


The next CASC is

CASC-J7

to be held at the 7th IJCAR as part of the Vienna Summer of Logic


Previous CASCs' Division Winners

THF TFA FOF FNT CNF SAT EPR UEQ LTB   T-Shirt Design
CASC‑24 (2013)   Satallax‑MaLeS 1.2 SPASS+T 2.2.19 Vampire 2.6 iProver 1.0‑SAT
-
-
iProver 0.9
-
MaLARea 0.5   Brain
CASC‑J6 (2012)   Isabelle 2012 Princess 120604 Vampire 2.6 Paradox 3.0
-
-
iProver 0.9
-
Vampire 2.6   Troll
CASC‑23 (2011)   Satallax 2.1 SPASS+T 2.2.14 Vampire 0.6 Paradox 3.0 E 1.4pre
-
iProver 0.9 Waldmeister 710 Vampire‑LTB 1.8   Flower Power
CASC‑J5 (2010)   LEO‑II 1.2
-
Vampire 0.6 (A&P) Paradox 3.0 (A&M) Vampire 0.6
-
iProver 0.8 Waldmeister 710 Vampire‑LTB 0.6   Bagpipes
CASC‑22 (2009)   TPS 3.080227G1d
-
Vampire 11.0 (A&P) Paradox 3.0(A&M) Vampire 10.0 Paradox 3.0 iProver 0.7 Waldmeister C09a Vampire‑LTB 11.0   Guillotine
CASC‑J4 (2008)  
-
-
Vampire 10.0 (A&P) MetaProver 1.0(A)
Paradox 3.0(M)
Vampire 10.0 MetaProver 1.0 iProver 0.5 Waldmeister 806 SInE 0.3   'Roo and Koalas
CASC‑21 (2007)  
-
-
Vampire 9.0 (A&P) Paradox 2.2(A&M) Vampire 8.1 (A&P) Paradox 1.3 (A&M) Darwin 1.3 Waldmeister 806
-
  Fishing
CASC‑J3 (2006)  
-
-
Vampire 8.1 (A&P)
-
Vampire 8.1 (A&P) Paradox 1.3 (A&M) Darwin 1.3 Waldmeister 806
-
  CASC Beer
CASC‑20 (2005)  
-
-
Vampire 8.0 (A&P)
-
Vampire 8.0 (A&P) Paradox 1.3 (A&M) DCTP 10.21p Waldmeister 704
-
  ATP seems Impossible
CASC‑J2 (2004)  
-
-
Vampire 7.0 (A&P)
-
Vampire 7.0 (A&P) Gandalf c‑2.6‑SAT (A)
Paradox 1.0‑casc (M)
DCTP 10.21p Waldmeister 704
-
  Love and Hate
CASC‑19 (2003)  
-
-
Vampire 6.0
-
Vampire 6.0 (A&P) Gandalf c‑2.6‑SAT (A)
Paradox 1.0‑casc (M)
DCTP 1.3-SAT Waldmeister 702
-
  State Space Explosion
CASC‑18 (2002)  
-
-
Vampire 5.0
-
Vampire 5.0 (A&P) Gandalf c-2.5-SAT E‑SETHEO csp02 Waldmeister 702
-
  Rainbow
CASC‑JC (2001)  
-
-
E‑SETHEO csp01
-
E‑SETHEO csp01 (A)
VampireJC 2.0 (A&P)
GandalfSat 1.0 E‑SETHEO csp01 Waldmeister 601
-
SEM
  Wizard logos
CASC‑17 (2000)  
-
-
VampireFOF 1.0
-
E 0.6 GandalfSat 1.0
-
Waldmeister 600 E‑SETHEO csp00   Flying saucer
CASC‑16 (1999)  
-
-
SPASS 1.00T
-
Vampire 0.0 OtterMACE 437
-
Waldmeister 799
-
  Spray can
CASC‑15 (1998)  
-
-
SPASS 1.0.0a
-
Gandalf c‑1.1 SPASS 1.0.0a
-
Waldmeister 798
-
  Worm and butterfly
CASC‑14 (1997)  
-
-
SPASS 0.77
-
Gandalf SPASS 0.77
-
Waldmeister
-
  Meat mincer
CASC‑13 (1996)  
-
-
-
-
E-SETHEO
-
-
Otter 3.0.4z
-
   


If you would like to cite CASC (in general), please use:

@Article{SS06-SoCASC,
    Author       = "Sutcliffe, G. and Suttner, C.",
    Year         = "2006",
    Title        = "{The State of CASC}",
    Journal      = "AI Communications",
    Volume       = "19",
    Number       = "1",
    Pages        = "35-48"
}

@Article{PSS02,
    Author       = "Pelletier, F.J. and Sutcliffe, G. and Suttner, C.B.",
    Year         = "2002",
    Title        = "{The Development of CASC}",
    Journal      = "AI Communications",
    Volume       = "15",
    Number       = "2-3",
    Pages        = "79-90"
} 
Individual CASC reports are:
@Article{Sut13,
    Author       = "Sutcliffe, G.",
    Year         = "2013",
    Title        = "{The 6th IJCAR Automated Theorem Proving System Competition
                    - CASC-J6}",
    Journal      = "AI Communications",
    Volume       = "26",
    Number       = "2",
    Pages        = "211-223"
}

@Article{Sut12,
    Author       = "Sutcliffe, G.",
    Year         = "2012",
    Title        = "{The CADE-23 Automated Theorem Proving System Competition
                    - CASC-23}",
    Journal      = "AI Communications",
    Volume       = "25",
    Number       = "1",
    Pages        = "49-63"
}

@Article{Sut11,
    Author       = "Sutcliffe, G.",
    Year         = "2011",
    Title        = "{The 5th IJCAR Automated Theorem Proving System Competition
                    - CASC-J5}",
    Journal      = "AI Communications",
    Volume       = "24",
    Number       = "1",
    Pages        = "75-89"
}

@Article{Sut10,
    Author       = "Sutcliffe, G.",
    Year         = "2010",
    Title        = "{The CADE-22 Automated Theorem Proving System Competition -
                    CASC-22}",
    Journal      = "AI Communications",
    Volume       = "23",
    Number       = "1",
    Pages        = "47-60"
}

@Article{Sut09,
    Author       = "Sutcliffe, G.",
    Year         = "2009",
    Title        = "{The 4th IJCAR Automated Theorem Proving Competition}",
    Journal      = "AI Communications",
    Volume       = "22",
    Number       = "1",
    Pages        = "59-72"
}

@Article{Sut08,
    Author       = "Sutcliffe, G.",
    Year         = "2008",
    Title        = "{The CADE-21 Automated Theorem Proving System Competition}",
    Journal      = "AI Communications",
    Volume       = "21",
    Number       = "1",
    Pages        = "71-82"
}

@Article{Sut07,
    Author       = "Sutcliffe, G.",
    Year         = "2007",
    Title        = "{The 3rd IJCAR Automated Theorem Proving Competition}",
    Journal      = "AI Communications",
    Volume       = "20",
    Number       = "2",
    Pages        = "117-126"
}

@Article{Sut06,
    Author       = "Sutcliffe, G.",
    Year         = "2006",
    Title        = "{The CADE-20 Automated Theorem Proving Competition}",
    Journal      = "AI Communications",
    Volume       = "19",
    Number       = "2",
    Pages        = "173-181"
}

@Article{Sut05,
    Author       = "Sutcliffe, G.",
    Year         = "2005",
    Title        = "{The IJCAR-2004 Automated Theorem Proving Competition}",
    Journal      = "AI Communications",
    Volume       = "18",
    Number       = "1",
    Pages        = "33-40",
    Comment      = "TPTPData,TPTPCite"
}

@Article{SS04,
    Author       = "Sutcliffe, G. and Suttner, C.",
    Year         = "2004",
    Title        = "{The CADE-19 ATP System Competition}",
    Journal      = "AI Communications",
    Volume       = "17",
    Number       = "3",
    Pages        = "103-182"
}

@Article{SS03,
    Author       = "Sutcliffe, G. and Suttner, C.",
    Year         = "2003",
    Title        = "{The CADE-18 ATP System Competition}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "31",
    Number       = "1",
    Pages        = "23-32"
}

@Article{SSP02,
    Author       = "Sutcliffe, G. and Suttner, C. and Pelletier, F.J.",
    Year         = "2002",
    Title        = "{The IJCAR ATP System Competition}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "28",
    Number       = "3",
    Pages        = "307-320"
}

@Article{Sut01,
    Author       = "Sutcliffe, G.",
    Year         = "2001",
    Title        = "{The CADE-17 ATP System Competition}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "27",
    Number       = "3",
    Pages        = "227-250"
}

@Article{Sut00,
    Author       = "Sutcliffe, G.",
    Year         = "2000",
    Title        = "{The CADE-16 ATP System Competition}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "24",
    Number       = "3",
    Pages        = "371-396"
}

@Article{SS99,
    Author       = "Sutcliffe, G. and Suttner, C.B.",
    Year         = "1999",
    Title        = "{The CADE-15 ATP System Competition}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "23",
    Number       = "1",
    Pages        = "1-23"
}

@Article{SS98,
    Author       = "Suttner, C.B. and Sutcliffe, G.",
    Year         = "1998",
    Title        = "{The CADE-14 ATP System Competition}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "21",
    Number       = "1",
    Pages        = "99-134"
}

@Article{SS97,
    Author       = "Sutcliffe, G. and Suttner, C.B.",
    Year         = "1997",
    Title        = "{Special Issue: The CADE-13 ATP System Competition}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "18",
    Number       = "2"
}


Other people are doing similar things for other types of ATP problems:

The Competition on Software Verification

The Answer Set Programming System Competition

The Satisfiability Modulo Theories Competition.

A competition intended to improve understanding of the sources of solver efficiency, and the options that should be considered in crafting solvers.

A competition for systems for proving termination.

The purpose of the competition is to identify new challenging benchmarks and to promote new solvers for the propositional satisfiability problem (SAT) as well as to compare them with state-of-the-art solvers.

SAT-Race is a competitive event for solvers of the Boolean Satisfiability (SAT) problem. The focus of SAT-Race is on application benchmarks, with a limited time to solve each instance.

The objective of MaxSAT is assessing the state of the art in the field of Max-SAT solvers, as well as creating a collection of publicly available Max-SAT benchmark instances.

The goal of the pseudo-Boolean competition is to assess the state of the art in the field of pseudo-Boolean solvers.

The aim of the TABLEAUX Non Classical Systems Comparison (TANCS) is to compare the performance of fully automatic, non classical ATP systems (based on tableaux, resolution, rewriting, ...) in an experimental setting and promote the experimental study on theorem proving and satisfiability testing in non classical logics.

  • CISC

An informal competition between inductive theorem proving systems.

QBF Evaluations are a series of yearly events with the purpose of assessing the state of the art in the field of QBF solvers and QBF-based applications. The final of the evaluation are presented during the yearly SAT conferences.


Other people are doing similar things for other types of AI problems:

The SUMO prize for US$3000.00 is awarded each year to the best open source project that extends SUMO.

A General Game Playing System is one that can accept a formal description of an arbitrary game and, without further human interaction, can play the game effectively.

The Computational Logic in Multi-Agent (CLIMA) systems competition is an attempt to stimulate research in the area of multi-agent systems by identifying key problems and collecting suitable benchmarks that can serve as milestones for testing new approaches and techniques from computational logics.

The Robot World Cup Initiative is an international research and education initiative. It is an attempt to foster AI and intelligent robotics research by providing a standard problem where wide range of technologies can be integrated and examined, as well as being used for intergrated project-oriented education. For this purpose, RoboCup chose to use soccer game as a primary domain, and organizes RoboCup: The Robot World Cup Soccer Games and Conferences.

In the TAC shopping game, each "agent" (an entrant to the competition) is a travel agent, with the goal of assembling travel packages (from TACtown to Tampa, during a notional 5-day period). Each agent is acting on behalf of eight clients, who express their preferences for various aspects of the trip. The objective of the travel agent is to maximize the total satisfaction of its clients (the sum of the client utilities).

The objectives are to provide a forum for empirical comparison of planning systems, to highlight challenges to the community in the form of problems at the edge of current capabilities, to propose new directions for research and to provide a core of common benchmark problems and a representation formalism that can aid in the comparison and evaluation of planning systems. Although the series has a competitive style, the focus is on data-collection and presentation, with interpretation of results being understated.

The ICCA was founded by computer chess programmers in 1977 to organise championship events for computer programs and facilitate sharing of technical knowledge via the ICGA Journal (formerly the ICCA Journal). The ICCA also seeks to represent the Computer Chess World via contacts with Computer Science Organizations, Commercial i Organisations, and the International Chess Federation (FIDE).

The aim of this event is to compare the expressiveness, the usability and the performance of graph and model transformation tools. A deeper understanding of the relative merits of different tool features will help to further improve graph and model transformation tools and to indicate open problems.

The Loebner Prize is the first formal instantiation of a Turing Test. In 1990 Hugh Loebner agreed with The Cambridge Center for Behavioral Studies to underwrite a contest designed to implement the Turing Test. Dr. Loebner pledged a Grand Prize of $100,000 and a Gold Medal for the first computer whose responses were indistinguishable from a human's. Each year an annual prize of $2000 and a bronze medal is awarded to the most human computer. The winner of the annual contest is the best entry relative to other entries that year, irrespective of how good it is in an absolute sense.