Matematickou olympiádu máme všichni v živé paměti. Žáci se v zadaném čase snaží správně vyřešit maximum matematických úloh. Obdobně funguje i světový šampionát v automatickém dokazování.
Konkrétně se jedná o šampionát nazvaný The CADE ATP System Competition, který již řadu let organizuje Dr. Geoff Sutcliffe z Univerzity v Miami, a který je součástí mezinárodní konference automatického uvažování (ta letošní, The 29th International Conference on Automated Deduction, se konala v italském Římě ve dnech 1. – 4. července). Jen úlohy na šampionátu nejsou formulovány v přirozeném, ale ve strojově srozumitelném jazyce matematické logiky a namísto žáků je řeší naprogramované systémy s prvky umělé inteligence, které bychom s trochou fantazie mohli přirovnat k automatickému matematikovi. Systémy se v rámci časového limitu 3 nebo 5 minut snaží vyřešit maximální množství náhodně vybraných matematických problémů.
Šampionát v automatickém dokazování ovšem není jen soutěží algoritmů nebo soubojem o to, kdo dokáže posunout limity tohoto vědeckého oboru o největší kus. Automatické dokazování může ve svých aplikacích vést k důležitým výsledkům – dokazovače by mohly usnadnit nebo ulehčit práci matematikům, logikům, programátorům, designérům systémů (software, hardware, komunikační protokoly) apod. To poslední je obzvláště důležité v případě systémů, na jejichž správném a spolehlivém fungovaní závisí lidské životy, jako například v medicíně nebo v dopravě.
Jedním z velmi úspěšných systémů na šampionátu je dlouhodobě Vampire, na kterém se podílí také Martin Suda, vedoucí skupiny automatického uvažování na CIIRC ČVUT. Vampire a jeho nejnovější verze 4.8 vyhrál kategorie First-order Non-theorems, Typed First-Order Non-Theorems, Typed First-order Theorems a také kategorii Higher-order Theorems. Poslední zmiňovaná kategorie aktuálně představuje pro vědce zajímavou výzvu v oblasti logiky vyššího řádu, která je daleko výrazově bohatší než standardně studovaná logika prvního řádu, zároveň je ale uvažování v ní o tolik složitější, že byla do nedávné doby považována za pro automatizaci nevhodnou.
Na vývoji systému Vampire pro logiku vyššího řádu se kromě Martina Sudy, který vytvořil portfolio strategií, zejména zasloužil Ahmed Bhayat z University v Manchesteru.
Výsledky lze nalézt ZDE.
Zdroj: tým Vampire
