Detalle del congreso

Autores: Cristiá, Maximiliano; Rossi, Gianfranco.

Resumen: In this paper we present a decision procedure for sets, binary relations and partial functions. The language accepted by the decision procedure includes untyped, hereditarily finite sets, where some of their elements can be variables, and basically all the classic set and relational operators used in formal languages such as B and Z. Partial functions are encoded as binary relations which in turn are just sets of ordered pairs. Sets are first-class entities in the language, thus they are not encoded in lower level theories. The decision procedure exploits set unification and set constraint solving as primitive features. The procedure is proved to be sound, complete and terminating. A Prolog implementation is presented.

Tipo de reunión: Conferencia.

Tipo de trabajo: Artículo Completo.

Producción: A decision procedure for sets, binary relations and a partial functions.

Reunión científica: 28th International Conference on Computer Aided Verification.

Lugar: Toronto.

Publicado: Sí

Lugar publicación: Berlin

Mes de reunión: 7

Año: 2016.