The Logical Approach to Automatic Sequences: Exploring Combinatorics on Words with Walnut

Automatic 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.

自動序列是由有限狀態機生成的有限字母序列。本書提出了一種關於自動序列的新觀點，更廣泛地介紹了關於字串組合學的知識，通過引入一種決策方法，可以在很少或沒有人為干預的情況下自動證明或否定組合學和數論中的許多新結果。這種證明定理的方法非常強大，可以用簡單的計算取代冗長且容易出錯的基於案例的論證。讀者將學習如何用一階邏輯來表達他們所需的結果，並使用免費軟件自動化計算過程。通常需要多頁證明的結果可以在毫秒內得出，使用者能夠解決原本難以解決的數學問題。本書包含150多個練習題，是研究人員、研究生和高年級本科生學習組合學、序列和數論的理想資源。