Self-Verifying Predicates in Büchi Arithmetic

Mazen Khodier, Luke Schaeffer, Jeffrey Shallit

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üchi arithmetic. Cons…