Externí odkazy

Analýza důkazů a automatická dedukce pro rekurzivní struktury

GF22-06414L [Registrované výsledky] 2022 - 2025

Matematická indukce je jedna z základních nástrojů každého matematika. Ukázalo se ale, že komplikuje formální analýzu důkazů. Podstata indukce je, že komprimuje nekonečný argument do konečného výroku. Tento proces zamlžuje informaci, která je podstatná pro výpočetní transformaci důkazů a automatické uvažování. Herbrandova věta pokrývá klasickou predikátovou logiku, kde se tato informace dá reprezentovat v konečně podobě. Navíc se dá použít pro analýzu důkazů a jako formální základ pro automatické dokazování. Ačkoli jsou interpretace Herbrandové věty, které rozšíří její rozsah na formální teorii čísel, tyto výsledky se vzdají analyticity, která je důležitá vlastnost Herbrandové věty. Pokrok v porozumění hranice analyticity je kvůli stoupající důležitosti formální matematiky a dokazování induktivních teoremů v informatice podstatný.