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

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

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.

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 <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)

AF - Dokumentace, knihovnictví, práce s informacemi<br>BC - Teorie a systémy řízení<br>BD - Teorie informace<br>IN - Informatika

Zahájení řešení

1. 7. 2022

Ukončení řešení

31. 12. 2025

Poslední stav řešení

B - Běžící víceletý projekt

Poslední uvolnění podpory

5. 5. 2023

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

CEP24-GA0-GF-R

Datum dodání záznamu

19. 2. 2024

Celkové uznané náklady

4 185 tis. Kč

Výše podpory ze státního rozpočtu

4 185 tis. Kč

Ostatní veřejné zdroje financování

0 tis. Kč

Neveřejné tuz. a zahr. zdroje finan.

0 tis. Kč