Publikace na Matematicko-fyzikální fakulta |
2008
Abstrakt
Článek popisuje v současnosti nejsilnejší existující systém pro automatické dokazování vět nad velkými matematickými teoriemi jako je databáze Mizar. Systém propojuje sémantické metody založené na tvorbě a použití databáze modelů s metodami strojového učení z předchozích důkazů, a používá tyto metody pro výběr dostatečně malé množiny nejrelevantnejších axiomů vhodných pro důkaz hypotéz.
Tento systém zvítězil v kategorii řešení velkých matematických problémů (MZR) letošního (2008) ročníku soutěže automatických dokazovačů (CASC) v Sydney, a vyřešil 1.5-krát více problémů než druhý nejlepší systém v této kategorii.