Automated Proof (or Disproof) of Linear Recurrences Satisfied by Pisot Sequences

Shalosh B. Ekhad, N. J. A. Sloane, Doron Zeilberger

Pisot sequences (sequences $a_n$ with initial terms $a_0=x,a_1=y$, and defined for $n>1$ by $a_n=\lfloor a_{n-1}^2/a_{n-2}+\frac{1}{2}\rfloor$) often satisfy linear recurrence…