Universal quantification makes automatic structures hard to decide

DOI10.46298/LMCS-22(1:14)2026MaRDI QIDQ6840502zbMATH OpenFDO

Authors Christoph Haase, Radosław Piórkowski

Publication date 23 March 2026

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-22(1:14)2026

zbMATH Keywords

automatic structuresquantifier eliminationBüchi arithmeticuniversal projection

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• Automatic presentations of structures
• Automatic structures of bounded degree revisited
• Complexity hierarchies beyond elementary
• Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree
• Geometric decision procedures and the VC dimension of linear arithmetic theories
• Logic and p-recognizable sets of integers
• On direct products of automaton decidable theories
• On the complexity of quantified integer programming
• On the existential theories of Büchi arithmetic and linear p-adic fields
• On the expressiveness of Büchi arithmetic
• Programming Techniques: Regular expression search algorithm
• Semigroups, Presburger formulas, and languages
• Subclasses of Presburger arithmetic and the weak EXP hierarchy
• TaPAS: The Talence Presburger Arithmetic Suite
• Theories of Automatic Structures and Their Complexity
• Universal first-order quantification over automata
• Weak Second‐Order Arithmetic and Finite Automata
• Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.

This page was built for publication: Universal quantification makes automatic structures hard to decide

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6840502)