CADE ATP System Competition

CADE ATP System Competition (CASC, gdzie ATP to automated theorem proving) – zawody systemów automatycznego dowodzenia twierdzeń, organizowane w ramach konferencji CADE.

Programy dostają do rozwiązania problemy z biblioteki TPTP, przy czym wygrywa program który rozwiąże ich najwięcej w najkrótszym czasie.

Zawody odbywają się w kilkunastu kategoriach, różniących się rodzajami problemów, zależnie od takich kwestii jak:

• tylko klauzule Horna lub dowolne klauzule
• tylko równość, bez równości, i problemy mieszane
• problem w ogólnej postaci rachunku predykatów pierwszego rzędu lub w koniunkcyjnej postaci normalnej (CNF)
• specjalna kategoria dla rachunku zdań