The Logical Approach to Automatic Sequences: Exploring Combinatorics on Words with WalnutAutomatic sequences are sequences over a finite alphabet generated by a finite-state machine. This book presents a novel viewpoint on automatic sequences, and more generally on combinatorics on words, by introducing a decision method through which many new results in combinatorics and number theory can be automatically proved or disproved with little or no human intervention. This approach to proving theorems is extremely powerful, allowing long and error-prone case-based arguments to be replaced by simple computations. Readers will learn how to phrase their desired results in first-order logic, using free software to automate the computation process. Results that normally require multipage proofs can emerge in milliseconds, allowing users to engage with mathematical questions that would otherwise be difficult to solve. With more than 150 exercises included, this text is an ideal resource for researchers, graduate students, and advanced undergraduates studying combinatorics, sequences, and number theory. |
What people are saying - Write a review
We haven't found any reviews in the usual places.
Contents
1 | |
2 Words and sequences | 10 |
3 Number representations and numeration systems | 32 |
4 Automata | 47 |
5 Automatic sequences | 62 |
6 Firstorder logic and automatic sequences | 82 |
7 Using Walnut | 96 |
8 Firstorder formulas for fundamental sequence properties | 113 |
Other editions - View all
Common terms and phrases
abelian accepts addition algorithm alphabet appears asserts automatic sequences automaton base binary bound called combination command complexity compute consider constant construct contains corresponding count create defined determine DFAO distinct easily element eval evaluates exactly example Exercise exists exponent expression factor of length factors Fibonacci Fibonacci word Figure finite first-order follows formula function given gives Hence infinite infinite word input integer k-automatic k-regular language least length-n letters linear representation logical Math means minimal morphism msd_fib natural numbers nonempty Notes numeration system occurrences output palindromes paperfolding sequence period polynomial position possible prefix problem Proof prove Recall recognizing recurrent regular relations represented result returns Shallit Show squares starting Suppose symbol synchronized takes Theorem theory Thue-Morse sequence TRUE values variables verify Walnut write