Presburger arithmetic with unary predicates is Π11 complete

DOI10.2307/2274706MaRDI QIDQ3984438zbMATH OpenOpenAlexFDO

Authors Joseph Y. Halpern

Publication date 27 June 1992

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2307/2274706

zbMATH Keywords

complexity of logical theoriesextensions of Presburger arithmeticundecidability

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) Undecidability and degrees of sets of sentences (03D35) First-order arithmetic and fragments (03F30)

Recommendations

• A note on definability in fragments of arithmetic with free unary predicates
• On decidable extensions of Presburger arithmetic: from A. Bertrand numeration sytems to Pisot numbers
• Complexity of Presburger arithmetic with fixed quantifier dimension
• Publication:4508549

Cites work

• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• Propositional dynamic logic of nonregular programs
• The complexity of logical theories

Cited in

(28)

• Don't care words with an application to the automata-based approach for real addition
• Cardinality constraints for arrays (decidability results and applications)
• Superposition as a decision procedure for timed automata
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Array theory of bounded elements and its applications
• Counting constraints in flat array fragments
• Decision procedures for flat array properties
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Free variables and theories: revisiting rigid E-unification
• A new acceleration-based combination framework for array properties
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• Some new results in monadic second-order arithmetic
• A note on definability in fragments of arithmetic with free unary predicates
• Collapsing probabilistic hierarchies. I
• On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation
• On deciding satisfiability by theorem proving with speculative inferences
• Analyzing automata with Presburger arithmetic and uninterpreted function symbols
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• Notes on the computational aspects of Kripke's theory of truth
• Extending two-variable logic on data trees with order on data values and its automata
• A collapse result for extensions of the Presburger arithmetic by a one-place function compatible with addition.
• Elementary invariants for quantified probability logic
• Universal first-order quantification over automata
• Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
• Universal first-order quantification over automata
• Sharpening complexity results in quantified probability logic
• Representing hyper-arithmetical sets by equations over sets of integers

This page was built for publication: Presburger arithmetic with unary predicates is Π₁¹ complete

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