Formalizing a fragment of combinatorics on words

DOI10.1007/978-3-319-58741-7_3zbMATH Open1433.68579OpenAlexW2612612198MaRDI QIDQ2011632FDOQ2011632

Authors: Štěpán Holub, Robert Veroff 

Publication date: 4 August 2017

Full work available at URL: https://doi.org/10.1007/978-3-319-58741-7_3

zbMATH Keywords

combinatorics on wordsperiodicityautomated theorem provingformalization

Mathematics Subject Classification ID

Combinatorics on words (68R15) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• The Kepler Conjecture
• Elements of automata theory. Translated from the French by Reuben Thomas
• Theorem proving in large formal mathematics as an emerging AI field
• Title not available (Why is that?)
• Uniqueness Theorems for Periodic Functions
• Title not available (Why is that?)
• Binary equality sets are generated by two words
• Intricacies of simple word equations: an example
• Formal proof
• Title not available (Why is that?)
• Formalizing a fragment of combinatorics on words
• Title not available (Why is that?)

Cited In (4)

• Lyndon words formalized in Isabelle/HOL
• Formalizing a fragment of combinatorics on words
• Automatic Theorem-Proving in Combinatorics on Words
• Title not available (Why is that?)

Uses Software

• Prover9
• kepler98
• Combinatorics_Words

This page was built for publication: Formalizing a fragment of combinatorics on words

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