Analýza důkazů a automatická dedukce pro rekurzivní struktury
Cíle projektu
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ý.
Klíčová slova
Automated DeductionProof AnalysisInductionResolutionLogicPrimitive Recursion
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Mezinárodní grantové projekty hodnocené na principu LEAD Agency
Veřejná soutěž
—
Hlavní účastníci
Ústav informatiky AV ČR, v. v. i.
Druh soutěže
M2 - Mezinárodní spolupráce
Číslo smlouvy
22-06414L
Alternativní jazyk
Název projektu anglicky
Proof analysis AND Automated deduction FOr REcursive STructures
Anotace anglicky
Mathematical induction is one of the essential concepts in the mathematician's toolbox. Though, its use makes formal proof analysis difficult. In essence, induction compresses an infinite argument into a finite statement. This process obfuscates information essential for computational proof transformation and automated reasoning. Herbrand’s theorem covers classical predicate logic where this information can be finitely represented and used to analyze proofs and to provide a formal foundation for automated theorem proving. While there are interpretations of Herbrand’s theorem extending its scope to formal number theory, these results are at the expense of analyticity, the most desirable property of Herbrand’s theorem. Given the rising importance of formal mathematics and inductive theorem proving to many areas of computer science, developing our understanding of the analyticity boundary is essential.
Vědní obory
Kategorie VaV
ZV - Základní výzkum
OECD FORD - hlavní obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - vedlejší obor
—
OECD FORD - další vedlejší obor
—
CEP - odpovídající obory
(dle převodníku)AF - Dokumentace, knihovnictví, práce s informacemi
BC - Teorie a systémy řízení
BD - Teorie informace
IN - Informatika
Termíny řešení
Zahájení řešení
1. 7. 2022
Ukončení řešení
31. 12. 2025
Poslední stav řešení
K - Končící víceletý projekt
Poslední uvolnění podpory
1. 11. 2024
Dodání dat do CEP
Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP25-GA0-GF-R
Datum dodání záznamu
14. 3. 2025
Finance
Celkové uznané náklady
4 377 tis. Kč
Výše podpory ze státního rozpočtu
4 377 tis. Kč
Ostatní veřejné zdroje financování
0 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Uznané náklady
4 377 tis. Kč
Statní podpora
4 377 tis. Kč
0%
Poskytovatel
Grantová agentura České republiky
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Doba řešení
01. 07. 2022 - 31. 12. 2025