Presburger arithmetic with unary predicates is Π11 complete
From MaRDI portal
Publication:3984438
DOI10.2307/2274706zbMath0738.03017OpenAlexW1980102547MaRDI QIDQ3984438
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
Undecidability and degrees of sets of sentences (03D35) Complexity of computation (including implicit computational complexity) (03D15) First-order arithmetic and fragments (03F30)
Related Items
Decision procedures for flat array properties ⋮ Some new results in monadic second-order arithmetic ⋮ A note on definability in fragments of arithmetic with free unary predicates ⋮ Collapsing probabilistic hierarchies. I ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ Elementary invariants for quantified probability logic ⋮ 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 ⋮ Universal first-order quantification over automata ⋮ Superposition as a decision procedure for timed automata ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Extending two-variable logic on data trees with order on data values and its automata ⋮ Notes on the computational aspects of Kripke's theory of truth ⋮ Representing hyper-arithmetical sets by equations over sets of integers ⋮ Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic ⋮ Counting Constraints in Flat Array Fragments ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Don't care words with an application to the automata-based approach for real addition ⋮ Array theory of bounded elements and its applications
Cites Work
