Proof analysis AND Automated deduction FOr REcursive STructures
Project goals
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.
Keywords
Automated DeductionProof AnalysisInductionResolutionLogicPrimitive Recursion
Public support
Provider
Czech Science Foundation
Programme
—
Call for proposals
—
Main participants
Ústav informatiky AV ČR, v. v. i.
Contest type
M2 - International cooperation
Contract ID
22-06414L
Alternative language
Project name in Czech
Analýza důkazů a automatická dedukce pro rekurzivní struktury
Annotation in Czech
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ý.
Scientific branches
R&D category
ZV - Basic research
OECD FORD - main branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - secondary branch
—
OECD FORD - another secondary branch
—
AF - Documentation, librarianship, work with information
BC - Theory and management systems
BD - Information theory
IN - Informatics
Solution timeline
Realization period - beginning
Jul 1, 2022
Realization period - end
Dec 31, 2025
Project status
K - Ending multi-year project
Latest support payment
Nov 1, 2024
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP25-GA0-GF-R
Data delivery date
Mar 14, 2025
Finance
Total approved costs
4,377 thou. CZK
Public financial support
4,377 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
4 377 CZK thou.
Public support
4 377 CZK thou.
100%
Provider
Czech Science Foundation
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Solution period
01. 07. 2022 - 31. 12. 2025