Lyndon words formalized in Isabelle/HOL
From MaRDI portal
Publication:832940
DOI10.1007/978-3-030-81508-0_18OpenAlexW3193153727MaRDI QIDQ832940
Publication date: 25 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-81508-0_18
Related Items
Uses Software
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