Deciding Boolean algebra with Presburger arithmetic

DOI10.1007/s10817-006-9042-1zbMath1112.03011OpenAlexW2102913701MaRDI QIDQ861705

Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard

Publication date: 30 January 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://infoscience.epfl.ch/record/110248/files/KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic.pdf

zbMATH Keywords

complexityBoolean algebraquantifier eliminationprogram verificationdecision procedurePresburger arithmetic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Data structures (68P05)

Related Items (18)

NP satisfiability for arrays as powers ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ Logic-based ontology comparison and module extraction, with an application to DL-Lite ⋮ On algebraic array theories ⋮ A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals ⋮ Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars ⋮ Checking deadlock-freedom of parametric component-based systems ⋮ MUNCH - Automated Reasoner for Sets and Multisets ⋮ Unnamed Item ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ Using First-Order Theorem Provers in the Jahob Data Structure Verification System ⋮ Decision Procedures for Multisets with Cardinality Constraints ⋮ Sets with Cardinality Constraints in Satisfiability Modulo Theories ⋮ Counting Constraints in Flat Array Fragments ⋮ A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT ⋮ Effective Quantifier Elimination for Presburger Arithmetic with Infinity ⋮ Combining Theories with Shared Set Operations ⋮ Efficient automated reasoning about sets and multisets with cardinality constraints

Uses Software

• ML
• Isabelle/HOL
• VAMPIRE
• PVS
• UCLID
• HOL
• MONA
• Quaffle
• CVC Lite

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combining sets with cardinals
• Combining nonstably infinite theories
• Proof synthesis and reflection for linear arithmetic
• Complexity of Boolean algebras
• The complexity of logical theories
• The computational complexity of logical theories
• Logic and \(p\)-recognizable sets of integers
• Negative Boolean constraints
• Isabelle/HOL. A proof assistant for higher-order logic
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• Theory of computation.
• Solvable cases of the decision problem
• MONA IMPLEMENTATION SECRETS
• The first order properties of products of algebraic systems
• Simplification by Cooperating Decision Procedures
• Programming by Refinement, as Exemplified by the SETL Representation Sublanguage
• On the complexity of integer programming
• Alternation
• Transition predicate abstraction and fair termination
• Verification: Theory and Practice
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Computer Aided Verification
• Automated Deduction – CADE-20
• Presburger arithmetic with bounded quantifier alternation
• Advances in Databases and Information Systems
• Static Analysis
• An axiomatic basis for computer programming
• Generalized finite automata theory with an application to a decision problem of second-order logic
• Foundations of Software Science and Computational Structures
• Verification, Model Checking, and Abstract Interpretation
• Polynomial Constraints for Sets with Cardinality Bounds
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Deciding Boolean algebra with Presburger arithmetic