In the last few years novel connections between mathematical logic and automata theory have emerged. A question that often arises in this area is the following: given a numeration system of natural numbers, can addition in this numeration system be performed on a finite automaton? For example, it is well-known that addition of two natural numbers in binary representation can be carried out on a finite automaton.
The goal of this project is to study addition in non-standard numeration system (such as the Zeckendorf numeration system) and implement algorithms for addition in a theorem prover software Walnut (see https://github.com/hamousavi/Walnut). Following an idea championed by Jeffrey Shallit, this will then allow us to use this software to automatically prove new theorem about combinatorial properties of certain infinite words.
This is a continuation of the project "Automata and Numeration system" from the Fall semester 2018. Newcomers welcome!
Completion of Math 347 (or comparable) required. Basic knowledge of automata and coding ability helpful.