The First-Order Theory of Sets with Cardinality Constraints is Decidable

Details The First-Order Theory of Sets with Cardinality Constraints is Decidable The First-Order Theory of Sets with Cardinality Constraints is Decidable

2004-07-17

arxiv.org/abs/cs/0407045v2

Computer Science

Logic in Computer Science

18 pages

Scientific paper

We show that the decidability of the first-order theory of the language that combines Boolean algebras of sets of uninterpreted elements with Presburger arithmetic operations. We thereby disprove a recent conjecture that this theory is undecidable. Our language allows relating the cardinalities of sets to the values of integer variables, and can distinguish finite and infinite sets. We use quantifier elimination to show the decidability and obtain an elementary upper bound on the complexity. Precise program analyses can use our decidability result to verify representation invariants of data structures that use an integer field to represent the number of stored elements.

Affiliated with

Also associated with

No associations

Rating

The First-Order Theory of Sets with Cardinality Constraints is Decidable does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with The First-Order Theory of Sets with Cardinality Constraints is Decidable, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The First-Order Theory of Sets with Cardinality Constraints is Decidable will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-12030