Self-Verifying Predicates in Büchi Arithmetic

2025/07/25 by Khodier, Mazen, Schaeffer, Luke, Shallit, Jeffrey · 1 citation
#Combinatorics (math.CO) #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #FOS: Mathematics #Formal Languages and Automata Theory (cs.FL)

paper · doi:10.48550/arxiv.2507.19717

Abstract

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. Construction in this way can be faster and use much less space than more direct methods. We discuss the theory and we present some empirical data for the free software Walnut.

Citations

• Linear Recurrence Sequence Automata and the Addition of Abstract Numeration Systems
• Rarefied Thue-Morse Sums Via Automata Theory and Logic
• Rudin-Shapiro Sums Via Automata Theory and Logic
• Automatic Sequences in Negative Bases and Proofs of Some Conjectures of Shevelev
• Automatic Theorem Proving in Walnut

Cited by

• On a sequence of Kimberling and its relationship to the Tribonacci word

Related

• Congruence Relations for Büchi Automata
• Büchi automata recognizing sets of reals definable in first-order logic with addition and order
• Advanced Automata Minimization
• Model Checking Markov Chains Against Unambiguous Buchi Automata
• Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata