Lyndon words formalized in Isabelle/HOL
type: Item
instance of: scholarly article
title: Lyndon words formalized in Isabelle/HOL
DOI: 10.1007/978-3-030-81508-0_18
author: Štěpán Holub
author: Štěpán Starosta
publication date: 2022-03-25T00:00:00Z
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 7498728
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: Lyndon word
zbMATH Keywords: Lyndon factorization
zbMATH Keywords: combinatorics on words
describes a project that uses: Coq-Combi
describes a project that uses: Isabelle
describes a project that uses: Combinatorics_Words
describes a project that uses: Szpilrajn Extension
describes a project that uses: Isabelle/HOL
describes a project that uses: Archive Formal Proofs
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: 978-3-030-81508-0 18
OpenAlex ID: W3193153727
cites work: Mining the Archive of Formal Proofs
cites work: A new characterization of maximal repetitions by Lyndon trees
cites work: Hammering towards QED
cites work: Universal Lyndon Words
cites work: On generalized Lyndon words
cites work: 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)
cites work: Necklaces of beads in k colors and k-ary de Bruijn sequences
cites work: Without Loss of Generality
cites work: Binary intersection formalized
cites work: Formalizing a fragment of combinatorics on words
cites work: A survey of languages for formalizing mathematics
cites work: Q4341774
cites work: On Burnside's Problem
cites work: 2D Lyndon words and applications
cites work: Type Reconstruction for Type Classes
cites work: Q4003339
cites work: Formalizing Arrow's theorem
description: scientific article; zbMATH DE number 7498728