Automatic demonstration of mathematical conjectures

Abstract

A particular logic has been introduced for reasoning about automatic sequences. An automatic sequence is roughly speaking an infinite word that can be generated by a deterministic finite automaton. Properties of these sequences defined with quantifiers, logical operators, integer variables, addition, indexing on the sequence, and comparison operators are decidable. This work is focusing on a tool, Walnut, developed for automating decision procedures for this logic.

This tool allows to use natural numbers encoded in various numeration systems (binary, decimal, hexadecimal numeration systems are common in computer science). One interesting feature of the tool is the allowance to add new numeration systems if the addition automaton for this numeration system is provided. The user must thus provide an automaton accepting the language L = {(x,y,z)} with (x,y,z) being the encoding of three natural numbers in the numeration system, and such that the values represented by x and y added together give the value represented by z. The aim of this master thesis is to automate the generation of the addition automaton for the Fibonacci numeration systems. An original solution has been developed for this problem using automata. This new method is inspired from existing work, ensuring some interesting efficiency properties. A working implementation has been provided in order to generate the addition automaton in a dot file.