CADE ATP System Competition
(Przekierowano z CASC)
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ń