Quantifier-Elimination for the First-Order Theory of Boolean Algebras with Linear Cardinality Constraints

Abstract. We present for the first-order theory of atomic Boolean algebras of sets with linear cardinality constraints a quantifier elimination algorithm. In the case of atomic Boolean algebras of sets, this is a new generalization of Boole's well-known variable elimination method for conjunctions of Boolean equality constraints. We also explain the connection of this new logical result with the evaluation of relational calculus queries on constraint databases that contain Boolean linear cardinality constraints.

• Type: Conference
• Year: 2004
• Where: ADBIS
• Authors: Peter Z. Revesz
• Keywords: ADBIS 2004, Atomic Boolean Algebras, Boolean Equality Constraints, Database, Linear Cardinality Constraints