Formalizace kombinatoriky na slovech

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

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.

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

BI - Akustika a kmity

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

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

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č