A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
From MaRDI portal
Publication:2817912
DOI10.1007/978-3-319-40229-1_7zbMath1475.68430MaRDI QIDQ2817912
Cesare Tinelli, Kshitij Bansal, Andrew Reynolds, Clark Barrett
Publication date: 5 September 2016
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-40229-1_7
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Related Items
Unnamed Item, Improving automation for higher-order proof steps, Cardinality constraints for arrays (decidability results and applications), Checking deadlock-freedom of parametric component-based systems, Synthesizing precise and useful commutativity conditions
Uses Software
Cites Work
- Deciding Boolean algebra with Presburger arithmetic
- Sets with Cardinality Constraints in Satisfiability Modulo Theories
- Solving SAT and SAT Modulo Theories
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Polite Theories Revisited
- Unnamed Item
- Unnamed Item
- Unnamed Item