Formalizace kombinatoriky na slovech
Cíle projektu
Kombinatorika na slovech je oblast diskrétní matematiky, která jako jiné kombinatorické obory přirozeně tíhne k technickým a pracným důkazům, často obsahujícím opakování podobných úvah a rozsáhlé rozbory případů. Jako taková je vhodná k počítačově ověřitelné formalizaci, o kterou se však dosud nikdo vážněji nepokusil. Naším úmyslem je formalizovat základní teorii konečných slov v dokazovacím asistentu Isabelle/HOL a poté se zaměřit na rozsáhlý projekt klasifikace binárních ekvivalenčních slov, který svou komplexností již naráží na meze běžné lidské kontroly. Projekt jednak nepochybným způsobem zpřístupní existující výsledky, jednak bude ohledávat jejich hranice a testovat schonost automatických dokazovacích nástrojů nalézat v této oblasti nová fakta, nebo alespoň urychlit lidský výzkum.
Klíčová slova
combinatorics on wordsformal proofsautomated reasoningbinary equality languages
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Standardní projekty
Veřejná soutěž
SGA0202000001
Hlavní účastníci
Univerzita Karlova / Matematicko-fyzikální fakulta
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
20-20621S
Alternativní jazyk
Název projektu anglicky
Combinatorics on words formalization
Anotace anglicky
Combinatorics on words is an area of discrete mathematics and like other combinatorial fields it naturally tends to technical and tedious proofs that often repeat similar arguments and contain complex case analysis. As such it is suitable for a computer verifiable formalization, which however has not been seriously attempted so far. Our intention is to formalize basic theory of combinatorics on words in the proof assistant Isabelle/HOL, and then to focus on the vast project of classification of binary equality words, whose complexity is on the borderline of human control. The project will provide an incontestable presentation of existing results, will explore their boundaries, and test capability of automated provers to find new facts in this area, or at least to accelerate human research.
Vědní obory
Kategorie VaV
ZV - Základní výzkum
OECD FORD - hlavní obor
10307 - Acoustics
OECD FORD - vedlejší obor
—
OECD FORD - další vedlejší obor
—
CEP - odpovídající obory
(dle převodníku)BI - Akustika a kmity
Termíny řešení
Zahájení řešení
1. 1. 2020
Ukončení řešení
30. 6. 2023
Poslední stav řešení
—
Poslední uvolnění podpory
1. 4. 2023
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
CEP24-GA0-GA-R
Datum dodání záznamu
21. 5. 2024
Finance
Celkové uznané náklady
3 777 tis. Kč
Výše podpory ze státního rozpočtu
3 741 tis. Kč
Ostatní veřejné zdroje financování
36 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Základní informace
Uznané náklady
3 777 tis. Kč
Statní podpora
3 741 tis. Kč
99%
Poskytovatel
Grantová agentura České republiky
OECD FORD
Acoustics
Doba řešení
01. 01. 2020 - 30. 06. 2023