This thesis investigates properties of the Narayana sequence, a combinatorial sequence with recursive and morphic structure. We prove several known characteristics of the sequence. We then introduce the Walnut Prover, a tool for automating logical reasoning over automatic sequences. We describe its capabilities and limitations, and apply it to explore additional properties of the Narayana sequence.