Lyndon words formalized in Isabelle/HOL

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

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

Publication date: 25 March 2022

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

Recommendations

• Transfinite Lyndon words
• Transfinite Lyndon words
• Nyldon words
• 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)
• Fast machine words in Isabelle/HOL

zbMATH Keywords

Lyndon wordcombinatorics on wordsIsabelle/HOLLyndon factorization

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Cites Work

• Mining the Archive of Formal Proofs
• Necklaces of beads in k colors and k-ary de Bruijn sequences
• Title not available (Why is that?)
• On Burnside's Problem
• Title not available (Why is that?)
• 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)
• 2D Lyndon words and applications
• A new characterization of maximal repetitions by Lyndon trees
• On generalized Lyndon words
• Formalizing a fragment of combinatorics on words
• A survey of languages for formalizing mathematics
• Binary intersection formalized
• Universal Lyndon Words
• Without Loss of Generality
• Type Reconstruction for Type Classes
• Hammering towards QED

Cited In (2)

• Lyndon words
• Word equations in the context of string solving

Uses Software

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

This page was built for publication: Lyndon words formalized in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832940)