Pecan: An Automated Theorem Prover for Automatic Sequences using B\"uchi Automata
Reed Oei, Dun Ma, Christian Schulz, and Philipp Hieronymi
TL;DR
Pecan is an automated theorem prover designed to reason about properties of Sturmian words, enabling efficient proofs of complex mathematical theorems in combinatorics on words.
Contribution
It introduces Pecan, a novel automated theorem proving tool specifically tailored for properties of Sturmian words using Büchi automata.
Findings
Successfully proves non-trivial theorems about Sturmian words
Demonstrates efficiency in reasoning about infinite sequences
Advances automated reasoning in combinatorics on words
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
Topicssemigroups and automata theory · Algorithms and Data Compression · Logic, programming, and type systems