A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT

DOI10.1007/978-3-319-40229-1_7zbMath1475.68430OpenAlexW2505706330MaRDI 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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Improving automation for higher-order proof steps ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ Synthesizing precise and useful commutativity conditions ⋮ Checking deadlock-freedom of parametric component-based systems ⋮ Unnamed Item

Uses Software

• Leon
• CVC4

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

This page was built for publication: A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT