Publication

On Decision Procedures for Ordered Collections

2010
Reports

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, and 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 problems of set algebra, and 3) reasoning about constraints on orderings arising in termination proofs.

Official source

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

2010
Reports

Abstract

Official source

Related concepts (32)

Total order

In mathematics, a total order or linear order is a partial order in which any two elements are comparable. That is, a total order is a binary relation on some set , which satisfies the following for all and in : (reflexive). If and then (transitive). If and then (antisymmetric). or (strongly connected, formerly called total). Reflexivity (1.) already follows from connectedness (4.), but is required explicitly by many authors nevertheless, to indicate the kinship to partial orders.

Binary relation

In mathematics, a binary relation associates elements of one set, called the domain, with elements of another set, called the codomain. A binary relation over sets X and Y is a new set of ordered pairs (x, y) consisting of elements x in X and y in Y. It is a generalization of the more widely understood idea of a unary function. It encodes the common concept of relation: an element x is related to an element y, if and only if the pair (x, y) belongs to the set of ordered pairs that defines the binary relation.

Connected relation

In mathematics, a relation on a set is called connected or complete or total if it relates (or "compares") all pairs of elements of the set in one direction or the other while it is called strongly connected if it relates pairs of elements. As described in the terminology section below, the terminology for these properties is not uniform. This notion of "total" should not be confused with that of a total relation in the sense that for all there is a so that (see serial relation).

Related publications (1)

On Decision Procedures for Ordered Collections

Chat with Graph Search

Achieving Efficient Work-Stealing for Data-Parallel Collections