In 2016, Hamoon Mousavi published Walnut which is a program that implements automated theorem proving of propositions about automatic sequences. The main purpose of this thesis was to show the theoretical functi- onality of Walnut on the basis of the relation between automatic sequences and Presburger (resp. B¨uchi) arithmetic that is a decidable theory. Another goal was to describe adequately how the decision procedure of Walnut really works, and finally, to show the practical use of Walnut on several particular problems. One of these particular problems that are solved in the thesis is computation of the critical exponent of the Rudin-Shapiro sequence - this exercise was presented as an open problem in a book of 2003 (however, this exercise does not belong among open problems any more since Shallit proved in 2011 that the critical exponent is computable for all automatic sequences.) The last chapter itself can be also used as a brief manual for newcomers to Walnut that want to use this program for their own applications. 1
| Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:367670 |
| Date | January 2017 |
| Creators | Fišer, Jan |
| Contributors | Holub, Štěpán, Chvalovský, Karel |
| Source Sets | Czech ETDs |
| Language | Czech |
| Detected Language | English |
| Type | info:eu-repo/semantics/masterThesis |
| Rights | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.0015 seconds