Pages that link to "Item:Q3984438"
From MaRDI portal
The following pages link to Presburger arithmetic with unary predicates is <i>Π</i><sub>1</sub><sup>1</sup> complete (Q3984438):
Displayed 22 items.
- Decision procedures for flat array properties (Q287272) (← links)
- A note on definability in fragments of arithmetic with free unary predicates (Q365661) (← links)
- Collapsing probabilistic hierarchies. I (Q384407) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- Notes on the computational aspects of Kripke's theory of truth (Q526739) (← links)
- Representing hyper-arithmetical sets by equations over sets of integers (Q693054) (← links)
- Don't care words with an application to the automata-based approach for real addition (Q1028730) (← links)
- Cardinality constraints for arrays (decidability results and applications) (Q1688541) (← links)
- Superposition as a decision procedure for timed automata (Q1949086) (← links)
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates (Q2031420) (← links)
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (Q2058375) (← links)
- Array theory of bounded elements and its applications (Q2351149) (← links)
- Counting Constraints in Flat Array Fragments (Q2817911) (← links)
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic (Q2961583) (← links)
- Free Variables and Theories: Revisiting Rigid E-unification (Q2964448) (← links)
- A New Acceleration-Based Combination Framework for Array Properties (Q2964461) (← links)
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Q3075472) (← links)
- Some new results in monadic second-order arithmetic (Q3195649) (← links)
- Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols (Q4921500) (← links)
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving (Q5191095) (← links)
- Extending two-variable logic on data trees with order on data values and its automata (Q5410335) (← links)
- Elementary invariants for quantified probability logic (Q6095192) (← links)
