Combinatorics on words formalization
Project goals
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.
Keywords
combinatorics on wordsformal proofsautomated reasoningbinary equality languages
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
SGA0202000001
Main participants
Univerzita Karlova / Matematicko-fyzikální fakulta
Contest type
VS - Public tender
Contract ID
20-20621S
Alternative language
Project name in Czech
Formalizace kombinatoriky na slovech
Annotation in Czech
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.
Scientific branches
Solution timeline
Realization period - beginning
Jan 1, 2020
Realization period - end
Jun 30, 2023
Project status
—
Latest support payment
Apr 1, 2023
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
CEP24-GA0-GA-R
Data delivery date
May 21, 2024
Finance
Total approved costs
3,777 thou. CZK
Public financial support
3,741 thou. CZK
Other public sources
36 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
3 777 CZK thou.
Public support
3 741 CZK thou.
99%
Provider
Czech Science Foundation
OECD FORD
Acoustics
Solution period
01. 01. 2020 - 30. 06. 2023