Ordered Sets in the Calculus of Data Structures

Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of constraints in a modular way, by combining multiple decidable classes. Working with quantifierfree combinations of constraints makes the combination agenda more realistic and the resulting logics more likely to be tractable than in the presence of quantifiers. Our approach to combination is based on reducing decidable fragments to a common class, Boolean Algebra with Presburger Arithmetic (BAPA). This logic was introduced by Feferman and Vaught in 1959 and can express properties of uninterpreted sets of elements, with set algebra operations and equicardinality relation (consequently, it can also express Presburger arithmetic constraints on cardinalities of sets). Combination by reduction to BAPA allows us to obtain decidable quantifi...

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Viktor Kuncak, Ruzica Piskac, Philippe Suter
• Keywords: Automated Reasoning, CSL 2010, Decidable Quantifier-free Classes, Logic, Multiple Decidable Classes