Presburger arithmetic with unary predicates is Π11 complete
From MaRDI portal
Publication:3984438
DOI10.2307/2274706zbMath0738.03017MaRDI 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
03D35: Undecidability and degrees of sets of sentences
03D15: Complexity of computation (including implicit computational complexity)
03F30: First-order arithmetic and fragments
Related Items
Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols, On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving, Extending two-variable logic on data trees with order on data values and its automata, Elementary invariants for quantified probability logic, Decision procedures for flat array properties, A note on definability in fragments of arithmetic with free unary predicates, Collapsing probabilistic hierarchies. I, On deciding satisfiability by theorem proving with speculative inferences, Notes on the computational aspects of Kripke's theory of truth, Representing hyper-arithmetical sets by equations over sets of integers, 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, 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
Cites Work
