Approaching Arithmetic Theories with Finite-State Automata

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.

SUBMITTER: Leporati A 

PROVIDER: S-EPMC7206625 | biostudies-literature | 2020 Jan

REPOSITORIES: biostudies-literature