Formalizing a fragment of combinatorics on words

DOI10.1007/978-3-319-58741-7_3MaRDI QIDQ2011632zbMATH OpenOpenAlexFDO

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

• scientific article; zbMATH DE number 3710436 (Why is no real title available?)
• scientific article; zbMATH DE number 1948502 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• scientific article; zbMATH DE number 3099365 (Why is no real title available?)
• Binary equality sets are generated by two words
• Elements of automata theory. Translated from the French by Reuben Thomas
• Formal proof
• Formalizing a fragment of combinatorics on words
• Intricacies of simple word equations: an example
• The Kepler Conjecture
• Theorem proving in large formal mathematics as an emerging AI field
• Uniqueness Theorems for Periodic Functions

Cited in

(4)

• scientific article; zbMATH DE number 7407638 (Why is no real title available?)
• Lyndon words formalized in Isabelle/HOL
• Automatic Theorem-Proving in Combinatorics on Words
• Formalizing a fragment of combinatorics on words

Describes a project that uses

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)