An automated theorem prover is a program that takes as input a statement and proves (or disproves) it. Theorem provers can be very useful: computers are reliable and fast, allowing us to explore new ideas easily. Though it is impossible to prove all statements automatically, theorem provers can still solve many interesting problems.

Over the past two semesters, we developed the Pecan theorem prover, which can automatically prove statements expressed via Büchi automata, a model of computation that can handle infinitely long inputs. We have used Pecan to expand on prior work on automatically proving properties of Sturmian words. Pecan can prove theorems about all Sturmian words, an improvement over previous techniques that could only prove properties of restricted sets of Sturmian words.

Try out Pecan at http://reedoei.com/pecan