On Decision Procedures for Ordered Collections

paper ps   
We describe a decision procedure for a logic that supports 1) finite collections of elements (sets or multisets) 2) the cardinality operator 3) a total order relation on elements, 4) min and max operators on entire collections. Among the applications of this logic are 1) reasoning about the externally observable behavior of data structures such as random access priority queues, 2) specifying witness functions for synthesis problem of set algebra, and 3) reasoning about constraints on orderings arising in termination proofs.

Citation

Ruzica Piskac, Philippe Suter, and Viktor Kuncak. On decision procedures for ordered collections. Technical Report LARA-REPORT-2010-001, EPFL, 2010.

BibTex Entry

@techreport{PiskacETAL10DecisionProceduresforOrderedCollections,
  author = {Ruzica Piskac and Philippe Suter and Viktor Kuncak},
  title = {On Decision Procedures for Ordered Collections},
  institution = {EPFL},
  year = 2010,
  number = {LARA-REPORT-2010-001},
  abstract = {
We describe a decision procedure for a logic that supports
1) finite collections of elements (sets or multisets) 2)
the cardinality operator 3) a total order relation on elements,
4) min and max operators on entire collections. Among the
applications of this logic are 1) reasoning about the
externally observable behavior of data structures such as
random access priority queues, 2) specifying witness functions for
synthesis problem of set algebra, and 3) reasoning about
constraints on orderings arising in termination proofs.
}
}