A Decision Procedure for Restricted Intensional Sets

ROSSI, GIANFRANCO; MAXIMILIANO CRISTIÁ

Gotemburgo

Conferencia; 26th International Conference on Automated Deduction; 2017

In this paper we present a decision procedure for RestrictedIntensional Sets (RIS), i.e. sets given by a property rather than by enu-merating their elements, similar to set comprehensions available in speci-fication languages such as B and Z. The proposed procedure is parametricwith respect to a first-order language and theory X , providing at leastequality and a decision procedure to check for satisfiability of X -formulas.We show how this framework can be applied when X is the theory ofhereditarily finite sets as is supported by the language CLP(SET ). Wealso present a working implementation of RIS as part of the {log} tooland we show how it compares with a mainstream solver and how it helpsin the automatic verification of code fragments.