Related papers: Proving Properties of $\varphi$-Representations wi…
We prove a few new properties of the $\varphi$-representation of integers, where $\varphi = (1+\sqrt{5})/2$. In particular, we prove a 2012 conjecture of Kimberling. As software assistants, we used the Walnut theorem-prover, and in one…
Let $\alpha = (1+\sqrt{5})/2$ and define the lower and upper Wythoff sequences by $a_i = \lfloor i \alpha \rfloor$, $b_i = \lfloor i \alpha^2 \rfloor$ for $i \geq 1$. In a recent interesting paper, Kawsumarng et al. proved a number of…
We provide a method, based on automata theory, to mechanically prove the correctness of many numeration systems based on Fibonacci numbers. With it, long case-based and induction-based proofs of correctness can be replaced by simply…
Walnut is a software that using automata can prove theorems in combinatorics on words about automatic sequences. We are able to apply this software to both prove new results as well as reprove some old results on avoiding squares and cubes…
We use the automatic theorem prover Walnut to resolve various open problems from the OEIS and beyond. Specifically, we clarify the structure of sequence A260311, which concerns runs of sums of upper Wythoff numbers. We extend a result of…
We look at the Stolarsky interspersions (such as the Wythoff array) one more time, this time using tools from automata theory. These tools allow easy verification of many of the published results on these arrays, as well as proofs of new…
In a recent talk of Robbert Fokkink, some conjectures related to the infinite Tribonacci word were stated by the speaker and the audience. In this note we show how to prove (or disprove) the claims easily in a "purely mechanical" fashion,…
We discuss an interesting sequence defined recursively; namely, sequence A105774 from the On-Line Encyclopedia of Integer Sequences, and study some of its properties. Our main tools are Fibonacci representation, finite automata, and the…
We explore the Ziv-Lempel and Crochemore factorizations of some classical automatic sequences making an extensive use of the theorem prover Walnut.
Venkatachala on the one hand, and Avdispahi\'c & Zejnulahi on the other, both studiied integer sequences with an unusual sum property defined in a greedy way, and proved many results about them. However, their proofs were rather lengthy and…
We introduce a new generalization of Euler's $\varphi$-function associated with a system of polynomials of several variables. We reprove by a short direct approach certain known related identities, and study some other special cases that do…
Let ftm = 0111010010001... be the analogue of the Thue-Morse sequence in Fibonacci representation. In this note we show how, using the Walnut theorem-prover, to obtain a measure of its complexity, previously studied by Jamet, Popoli, and…
We discuss a technique, based on Angluin's algorithm, for automatically generating finite automata for various kinds of useful first-order logic formulas in B\"uchi arithmetic. Construction in this way can be faster and use much less space…
We give a parametrization with perfect sets of the abstract Ellentuck theorem. The main tool for achieving this goal is a sort of parametrization of an abstract version of the Nash-Williams theorem. As corollaries, we obtain some known…
The proofs first generated by automated theorem provers are far from optimal by any measure of simplicity. In this paper I describe a technique for simplifying automated proofs. Hopefully this discussion will stimulate interest in the…
Mathematical theorems are human knowledge able to be accumulated in the form of symbolic representation, and proving theorems has been considered intelligent behavior. Based on the BHK interpretation and the Curry-Howard isomorphism, proof…
We describe a technique for mechanically proving certain kinds of theorems in combinatorics on words, using automata and a package for manipulating them. We illustrate our technique by solving, purely mechanically, an open problem of Currie…
We give another proof of a theorem of Fife - understood broadly as providing a finite automaton that gives a complete description of all infinite binary overlap-free words. Our proof is significantly simpler than those in the literature. As…
We present a proof of Roth's theorem that follows a slightly different structure to the usual proofs, in that there is not much iteration. Although our proof works using a type of density increment argument (which is typical of most proofs…
We prove the following version of the first incompleteness theorem that simultaneously strengthens Mostowski's theorem and Vaught's theorem: For any c.e. family $\{ T_i \}_{i \in \omega}$ of consistent extensions of Tarski, Mostowski and…