Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
DOI10.1007/978-3-540-73595-3_15zbMATH Open1213.03021OpenAlexW1607550340MaRDI QIDQ3608775FDOQ3608775
Authors: Viktor Kuncak, Martin C. Rinard 
Publication date: 6 March 2009
Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)
Full work available at URL: http://infoscience.epfl.ch/record/110254
Recommendations
- Deciding Boolean algebra with Presburger arithmetic
- scientific article; zbMATH DE number 1903342
- scientific article; zbMATH DE number 2090309
- Computer Aided Verification
- Optimal satisfiability checking for arithmetic \(\mu\)-calculi
- scientific article; zbMATH DE number 1979549
- Automated Deduction – CADE-20
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Publication:2767086
- Enrichments of Boolean algebras by Presburger predicates
Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Cited In (25)
- Counting Constraints in Flat Array Fragments
- Succinct ordering and aggregation constraints in algebraic array theories
- Title not available (Why is that?)
- How to tell easy from hard: complexities of conjunctive query entailment in extensions of \(\mathcal{ALC}\)
- Two variable logic with ultimately periodic counting
- Title not available (Why is that?)
- One-variable logic meets Presburger arithmetic
- Title not available (Why is that?)
- Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
- Automated Deduction – CADE-20
- On algebraic array theories
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- Colors Make Theories Hard
- Combining theories with shared set operations
- Cardinality constraints for arrays (decidability results and applications)
- Sets with cardinality constraints in satisfiability modulo theories
- Certified Reasoning with Infinity
- Deciding Boolean algebra with Presburger arithmetic
- Decision procedures for region logic
- Linear Arithmetic with Stars
- Title not available (Why is that?)
- Decision Procedures for Multisets with Cardinality Constraints
- NP satisfiability for arrays as powers
- The Support of Integer Optimal Solutions
- Computer Aided Verification
Uses Software
This page was built for publication: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608775)
