Lyndon words formalized in Isabelle/HOL

DOI10.1007/978-3-030-81508-0_18OpenAlexW3193153727MaRDI QIDQ832940

Štěpán Starosta, Štěpán Holub

Publication date: 25 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81508-0_18

zbMATH Keywords

combinatorics on wordsIsabelle/HOLLyndon wordLyndon factorization

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items

Word equations in the context of string solving, Lyndon words

Uses Software

• Isabelle
• Isabelle/HOL
• GitHub
• Archive Formal Proofs
• Coq-Combi
• Combinatorics_Words
• Szpilrajn Extension

Cites Work

• Unnamed Item
• Unnamed Item
• 2D Lyndon words and applications
• Formalizing Arrow's theorem
• Génération d'une section des classes de conjugaison et arbre des mots de Lyndon de longueur bornée. (Generation of a section of conjugation classes and trees of Lyndon words of bounded length)
• Necklaces of beads in k colors and k-ary de Bruijn sequences
• Formalizing a fragment of combinatorics on words
• A survey of languages for formalizing mathematics
• On generalized Lyndon words
• Binary intersection formalized
• Universal Lyndon Words
• Without Loss of Generality
• Mining the Archive of Formal Proofs
• Type Reconstruction for Type Classes
• Hammering towards QED
• A new characterization of maximal repetitions by Lyndon trees
• On Burnside's Problem