Self-Verifying Predicates in Büchi Arithmetic
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912502455992320 |
|---|---|
| author | Khodier, Mazen Schaeffer, Luke Shallit, Jeffrey |
| author_facet | Khodier, Mazen Schaeffer, Luke Shallit, Jeffrey |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_19717 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Self-Verifying Predicates in Büchi Arithmetic Khodier, Mazen Schaeffer, Luke Shallit, Jeffrey Formal Languages and Automata Theory Discrete Mathematics Combinatorics 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. |
| title | Self-Verifying Predicates in Büchi Arithmetic |
| topic | Formal Languages and Automata Theory Discrete Mathematics Combinatorics |
| url | https://arxiv.org/abs/2507.19717 |