Automatic Theorem-Proving in Combinatorics on Words
From MaRDI portal
Abstract: We describe a technique for mechanically proving certain kinds of theorems in combinatorics on words, using automata and a package for manipulating them. We illustrate our technique by solving, purely mechanically, an open problem of Currie and Saari on the lengths of unbordered factors in the Thue-Morse sequence.
Recommendations
- Automatic theorem-proving in combinatorics on words
- Formalization of Basic Combinatorics on Words
- Automata on Words
- Combinatorics of Finite Words and Suffix Automata
- Formalizing a fragment of combinatorics on words
- scientific article; zbMATH DE number 1738654
- On the number of abelian bordered words (with an example of automatic theorem-proving)
- Automata on infinite words and their applications in formal verification
- Automatic generation of theorems and proofs on enumerating consecutive-Wilf classes
- Proof of a conjecture on word complexity
Cites work
- A decision method for the recognizability of sets defined by number systems
- A note on bifix-free sequences (Corresp.)
- A proof of the extended Duval's conjecture
- Automatic Sequences
- Biinfinite words with maximal recurrent unbordered factors.
- Enumeration and decidable properties of automatic sequences
- Folds!
- scientific article; zbMATH DE number 3693558 (Why is no real title available?)
- scientific article; zbMATH DE number 1740032 (Why is no real title available?)
- Infinite 0-1 sequences without long adjacent identical blocks
- Inverse star, borders, and palstars
- Least Periods of Factors of Infinite Words
- Logic and p-recognizable sets of integers
- On the relation between periodicity and unbordered factors of finite words
- Periodicity and unbordered segments of words
- Periodicity and unbordered words
- Periodicity, repetitions, and orbits of an automatic sequence
- Relationship between the period of a finite word and the length of its unbordered segments
- Some Theorems on Fourier Coefficients
- Unbordered factors and Lyndon words
Cited in
(11)- Some combinatorial properties of the Thue-Morse sequence and a problem in semigroups
- Additive number theory via automata theory
- Decision algorithms for Fibonacci-automatic words. I: Basic results.
- A new approach to the paperfolding sequences
- Mechanical proofs of properties of the Tribonacci word
- On the number of unbordered factors
- Intertwining of complementary Thue-Morse factors
- Deciding game invariance
- On the number of abelian bordered words (with an example of automatic theorem-proving)
- Automatic theorem-proving in combinatorics on words
- Asymptotic normality and strong consistency of maximum quasi-likelihood estimates in generalized linear models
This page was built for publication: Automatic Theorem-Proving in Combinatorics on Words
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914707)