A Case Study in Meta-AUTOMATION: AUTOMATIC Generation of Congruence AUTOMATA For Combinatorial Sequences

Pecan is an automated theorem prover for reasoning about properties of Sturmian words, an important object in the field of combinatorics on words. It is capable of efficiently proving non-trivial mathematical theorems about all Sturmian words.

This article, dedicated to Herbert Saul Wilf on the occaison of his forthcoming 80-th birthday, describes two complementary approaches to enumeration, the "positive" and the "negative", each with its advantages and disadvantages. Both approaches are amenable to automation, and when applied to the currently active subarea, initiated in 2003 by Sergi Elizalde and Marc Noy, of enumerating consecutive-Wilf classes (i.e. consecutive pattern-avoidance) in permutations, were success...

We consider the growth, order, and finiteness problems for automaton (semi)groups. We propose new implementations and compare them with the existing ones. As a result of extensive experimentations, we propose some conjectures on the order of finite automaton (semi)groups.

This paper gives a concise introduction into the basic theory of {\omega}-automata (as of March 2014). The starting point are the different types of recurrence conditions, modes of operation (deterministic, nondeterministic, alternating automata), and directions (forward or backward automata). The main focus is on fundamental automata constructions, for instance, for boolean operations, determinization, disambiguation, and removing alternation. It also covers some algebraic a...

The 16th International Conference on Automata and Formal Languages (AFL 2023) was held in Eger, September 5-7, 2023. It was organized by the Eszterh\'azy K\'aroly Catholic University of Eger, Hungary, and the University of Szeged, Hungary. Topics of interest covered the theory and applications of automata and formal languages and related areas. This volume contains the texts of the 3 invited presentations and the 18 papers selected by the International Program Committee fro...

This paper is inspired by a seqfan post by Jeremy Gardiner. The post listed nine sequences with similar parities. In this paper I prove that the similarities are not a coincidence but a mathematical fact.

Number-conserving cellular automata are discrete dynamical systems that simulate interacting particles like e.g. grains of sand. In an earlier paper, I had already derived a uniform construction for all transition rules of one-dimensional number-conserving automata. Here I describe in greater detail how one can simulate the automata on a computer and how to find interesting rules. I show several rules that I have found this way and also some theorems about the space of number...

This is a survey of using Minsky machines to study algorithmic problems in semigroups, groups and other algebraic systems.

Automatic sequences have many properties that other sequences (in particular, non-uniformly morphic sequences) do not necessarily share. In this paper we survey a number of different methods that can be used to prove that a given sequence is not automatic. When the sequences take their values in the finite field ${\mathbb F}_q$, this also permits proving that the associated formal power series are transcendental over ${\mathbb F}_q(X)$.

We explore the Ziv-Lempel and Crochemore factorizations of some classical automatic sequences making an extensive use of the theorem prover Walnut.