Succinct ordering and aggregation constraints in algebraic array theories
From MaRDI portal
Publication:6561348
DOI10.1016/j.jlamp.2024.100978MaRDI QIDQ6561348
Publication date: 25 June 2024
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Forward and backward application of symbolic tree transducers
- Symbolic tree automata
- Decision procedures. An algorithmic point of view
- Solving \(\mathrm{LIA}^\star\) using approximations
- Deciding Boolean algebra with Presburger arithmetic
- The monadic second order theory of all countable ordinals
- The computational complexity of logical theories
- Cardinality constraints for arrays (decidability results and applications)
- Efficient automated reasoning about sets and multisets with cardinality constraints
- NP satisfiability for arrays as powers
- Carathéodory bounds for integer cones
- Tree acceptors and some of their applications
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- Refinement types for Haskell
- Dafny: An Automatic Program Verifier for Functional Correctness
- Decision Procedures for Automating Termination Proofs
- Sets with Cardinality Constraints in Satisfiability Modulo Theories
- The first order properties of products of algebraic systems
- An application of games to the completeness problem for formalized theories
- Weak Second‐Order Arithmetic and Finite Automata
- Cosmological lower bound on the circuit complexity of a small problem in logic
- Linear Arithmetic with Stars
- Ordered Sets in the Calculus of Data Structures
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Combining Theories with Shared Set Operations
- Simplification by Cooperating Decision Procedures
- On the complexity of integer programming
- Array Folds Logic
- Minimization of Symbolic Tree Automata
- Symbolic Automata Constraint Solving
- Computational Complexity
- Automated Deduction – CADE-20
- Logics with aggregate operators
- Tree Automata over Infinite Alphabets
- Automata, Languages and Programming
- On direct products of theories
- Verification, Model Checking, and Abstract Interpretation
- Variants and satisfiability in the infinitary unification wonderland
- On algebraic array theories
This page was built for publication: Succinct ordering and aggregation constraints in algebraic array theories
