Haase, C;
(2020)
Approaching Arithmetic Theories with Finite-State Automata.
In: Leporati, A and Martín-Vide, C and Shapira, D and Zandron, C, (eds.)
International Conference on Language and Automata Theory and Applications LATA 2020: Language and Automata Theory and Applications.
(pp. pp. 33-43).
Springer: Milan, Italy.
Preview |
Text
haa-20.pdf - Accepted Version Download (553kB) | Preview |
Abstract
The automata-theoretic approach provides an elegant method for deciding linear arithmetic theories. This approach has recently been instrumental for settling long-standing open problems about the complexity of deciding the existential fragments of Büchi arithmetic and linear arithmetic over p-adic fields. In this article, which accompanies an invited talk, we give a high-level exposition of the NP upper bound for existential Büchi arithmetic, obtain some derived results, and further discuss some open problems.
| Type: | Proceedings paper |
|---|---|
| Title: | Approaching Arithmetic Theories with Finite-State Automata |
| Event: | 14th International Conference, LATA 2020, Milan, Italy, March 4–6, 2020 |
| Location: | Milan |
| ISBN-13: | 978-3-030-40607-3 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-40608-0_3 |
| Publisher version: | https://doi.org/10.1007/978-3-030-40608-0_3 |
| Language: | English |
| Additional information: | This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. |
| Keywords: | Presburger arithmetic, Büchi arithmetic, Reachability ,Automatic structures |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10089571 |
Archive Staff Only
 |
View Item |
