Intensional sets are sets given by a property rather than by enumerating their elements, similar to set comprehensions available in speci cation languages such as B and MiniZinc. In a previous paper [3] we have presented a decision procedure for a rst-order logic language which provides Restricted Intensional Sets (RIS), i.e. a sub-class of intensional sets that are guaranteed to denote nite|though unbounded|sets. In this paper we show how RIS can be exploited as a convenient programming tool also in a more conventional setting, namely, an imperative O-O language. We do this by considering a Java library, called JSetL [14], that integrates the notions of logical variable, (set) uni cation and constraints that are typical of constraint logic programming languages into the Java language. We show how JSetL is naturally extended to accommodate for RIS and RIS constraints, and how this extension can be exploited, on the one hand, to support a more declarative style of programming, and on the other hand, to e ectively enhance the expressive power of the constraint language provided by the library.
Intensional sets, also called set comprehensions, are sets described by providing
a condition ' that is necessary and su cient for an element x to belong to
the set itself, i.e., f x : '[x] g, where x is a variable and ' is a rst-order
formula containing x. Intensional sets are widely recognized as a key feature
to describe complex problems. As a matter of fact, various speci cation (or
modeling) languages provide intensional sets as rst-class entities. For example,
some form of intensional sets are o ered by MiniZinc [
The processing of intensional sets in most of these proposals is based on the
availability of a set-grouping mechanism [
An example of this approach is flogg (pronounced `setlog'), a freely available
extended Prolog system that embodies the CLP language with sets CLP(SE T )
[
Example 1. The following formulas can be written in flogg using (general) intensional sets, but flogg is not able to process them adequately, due to some of the problems with set-grouping listed above: { S = f2; 4; 6g ^ S = fx : x 2 D ^ x mod 2 = 0g; i.e., S is the set of all even numbers belonging to an unknown set D; { C = A \ B ^ S = fx : x 2 A ^ x 2 Bg ^ C 6= S, i.e., S is the set of all elements in both sets A and B (A and B unknown sets).
If, on the contrary, the sets involved in the above formulas are completely speci ed sets, then flogg is able to perform set-grouping and hence to compute the correct answers. tu
Set-grouping is not always necessary to deal with intensional sets. For
example, given the formula t 2 fx : 'g, one could check whether it is satis able
or not by simply checking satis ability of '(t), i.e., of the instance of ' which
is obtained by replacing x by t. A very general proposal along these lines is
CLP(fDg) [
Recently, Cristia and Rossi [
The work in [
The paper is organized as follows. Sect. 2 introduces RIS informally through some examples. Sect. 3 brie y reviews the JSetL library and Sect. 4 presents the extension of JSetL with RIS. In Sect. 5 we start showing examples using JSetL to demonstrate the usefulness of RIS and RIS constraints to support declarative programming. Sect. 6 shows how RIS can be used to de ne and manipulate partial functions. In Sect. 7 we consider some extensions to RIS and we present examples showing their usefulness. Finally, in Sect. 8 we draw some conclusion. 2
In this section we introduce RIS in an informal, intuitive way, through a number of simple examples.
The language that embodies RIS, called LRIS , is a quanti er-free rst-order logic language which provides both RIS and extensional sets, along with basic operations on them, as primitive entities of the language. LRIS is parametric with respect to an arbitrary theory X , for which we assume a decision procedure for any admissible X -formula is available. Elements of LRIS sets are the objects provided by X , which can be manipulated through the primitive operators that X o ers (at least, X -equality). Hence, RIS in LRIS represent untyped unbounded nite hybrid sets, i.e., unbounded nite sets whose elements are of any sort. For the sake of convenience, we assume that the language of X , LX , provides the constant, function and predicate symbols of the theories of the integer numbers and ordered pairs.
LRIS provides the following set terms: a) the empty set, noted ;; b) extensional sets, noted fx t Ag, where x, called element part, is an X -term, and A, called set part, is an LRIS set term; and c) Restricted Intensional Sets (RIS), noted fc : D j F P [c]g, where c, called control term, is an X -term; D, called domain, is an LRIS set term; F , called lter, is an X -formula; and P , called pattern, is an X -term containing c. Both extensional sets and RIS can be partially speci ed because elements and sets can be variables. As a notational convenience, ft1 t ft2 t ftn t tg gg (resp., ft1 t ft2 t ftn t ;g gg) is written as ft1; t2; : : : ; tn t tg (resp., ft1; t2; : : : ; tng). When useful, the domain D can be represented also as an interval [m; n], m and n integer constants, which is intended as a shorthand for fm; m+1; : : : ; ng. RIS-literals are of the form A = B, A 6= B, e 2 A or e 2= A, where A and B are set terms and e is an X -term. RIS-formulas are built from RIS-literals using conjunction and disjunction.
An extensional set fxtAg is interpreted as fxg[A. A RIS term is interpreted as follows: if x1; : : : ; xn (n > 0) are all the variables occurring in c, then fc : D j F P [c]g denotes the set fy : 9x1 : : : xn(c 2 D ^ F ^ y =X P [c])g. Note that x1; : : : ; xn are bound variables whose scope is the RIS term itself. Also note that equality between y and the pattern P requires equality of the theory X .
In order to devise a decision procedure for LRIS , the control term c and the pattern P of RIS are restricted to be of speci c forms. Namely, if x and y are variables ranging on the domain of X , then c can be either x or (x; y), while P can be either c or (c; t) or (t; c), where t is any (uninterpreted/interpreted) X term, possibly involving the variables in c. As it will be evident from the various examples in the next sections, in spite of these restrictions, LRIS is still a very expressive language.
Example 2. The following are RIS-literals involving RIS terms: { fx : [ 2; 2] j x mod 2 = 0 xg = f 2; 0; 2g { (5; y) 2 fx : D j x > 0 (x; x x)g, where y and D are free variables { (5; 0) 62 f(x; y) : fP t Rg j y 6= 0 (x; y)g, where P and R are free variables, and fP t Rg is a set term denoting the set fP g [ R. tu When the pattern is the control term and the lter is true, they can be omitted (as in Z and B), although one must be present.
LRIS provides a complete constraint solver which is able to decide satis ability of any LRIS formulas. Precisely, the solver reduces any input formula to either false (hence, is unsatis able), or to an equi-satis able disjunction of formulas in a simpli ed form, called the solved form, which is guaranteed to be satis able (hence, is satis able). If is satis able, the answer computed by the solver constitutes a nite representation of all the concrete (or ground) solutions of the input formula.
{ The second formula of Ex. 2 is rewritten by the LRIS solver to the solved form formula y = 25 ^ D = f5 t N1g, where the second equality states that D must contain 5 and something else, denoted N1. { The rst formula of Ex. 1 can be written using RIS as S = f2; 4; 6g ^ S = fx : D j x mod 2 = 0g; this formula is rewritten by the solver to a solved form formula containing the constraint D = f2; 4; 6tN1g^fx : N1 j xmod2 = 0g = ;, where the second equality states that N1 cannot contain even numbers (note that this constraint has the obvious solution N1 = ;). tu It is worth noting that the LRIS solver is able to correctly solve all formulas of Ex. 1, written using RIS. Moreover, note that the formula fx : p(x)g = fx : q(x)g, which is undecidable when p and q have an in nite number of solutions, can be \approximated" using RIS as fx : D1 j p(x)g = fx : D2 j q(x)g, D1, D2 variables, which is a solved form formula admitting at least one solution, namely D1 = D2 = ;; hence it is simply returned unchanged by the solver. 3
JSetL [
In JSetL a (generic) logical variable is an instance of the class LVar. Basically, LVar objects can be manipulated through constraints, namely equality (eq), inequality (neq), membership (in) and not membership (nin) constraints. Logical variables can be either initialized or uninitialized. When the collection of possible values for a logical variable reduces to a singleton, this value becomes the value of the variable and the variable is initialized. Moreover, a logical variable can have an optional external name (i.e., a string) which can be useful when printing the variable and the possible constraints involving it.
Values associated with generic logical variables can be of any type. For some speci c domains, however, JSetL o ers specializations of the LVar data type, which provide further speci c constraints. In particular, for the domain of integers, JSetL o ers the class IntLVar, which extends LVar with a number of new methods and constraints speci c for integers. In particular, IntLVar provides integer comparison constraints such as < (lt), (le), etc.
Other important specializations of logical variables are the class LCollection and its derived subclasses, LSet (for Logical Sets) and LList (for Logical Lists). Values associated with LSet (LList) are objects of the java.util class Set (List). A number of constraints are provided to work with LSet (LList), which extend those provided by LVar. In particular, LSet provides equality and inequality constraints that account for the semantic properties of sets (namely, irrelevance of order and duplication of elements); moreover it provides constraints for many of the standard set-theoretical operations, such as union (union), intersection (inters), inclusion (subset), and so on.
LList l = new LList(); // an uninitialized logical list LSet r = new LSet("r"); // an uninitialized logical set
// with external name "r" LVar x = new LVar("x"); LSet s2 = r.ins(x); LSet s1 = LSet.empty().ins(2).ins(1); // the set f1,2g
// the set fxg [ r LVar x = new LVar();
// an uninitialized logical variable LVar y = new LVar("y",1); // an initialized logical variable // with external name "y" and value 1 ins is the element insertion method for LSet objects: s.ins(o) returns the new logical set whose elements are those of the set s [ fog. In particular, the last statement in Ex. 5 creates a partially speci ed set s2 with an unknown element x and an unknown rest r (i.e., fx j rg, using a Prolog-like notation).
A JSetL constraint solver is an instance of the class SolverClass. Basically, it provides methods for adding constraints to its constraint store (e.g., the method add) and to prove constraint satis ability (e.g., the method solve). If solver is a solver,
is the collection of constraints stored in its constraint store (possibly empty), and c is a constraint, then solver.solve(c) checks whether ^ c is satis able or not: if it is, then the constraint store is modi ed so to represent the computed constraint in solved form; otherwise an exception Failure is raised.
LVar x = new LVar("x"), y = new LVar("y"); LSet s1 = LSet.empty().ins(2).ins(1); // the set f1,2g LSet s2 = LSet.empty().ins(y).ins(x); // the set fx,yg tu tu SolverClass solver = new SolverClass(); solver.solve(); x.output(); y.output(); // the constraint s1=s2 ^ x6=1 where the method output is used to print the value possibly bound to a logical object. Executing this code fragment will output: x = 2, y = 1. 4
tu tu tu the control term. follows: In this section we show how RIS are added to JSetL. The new version of the JSetL library can be downloaded from the JSetL's home page. All sample Java programs shown in this and in the next sections have been tested using the new version and are available on-line.
RIS are added to JSetL by de ning a new class, named Ris. Ris extends
LSet, hence Ris objects can be used as logical sets, and all methods of LSet
are inherited by Ris. Basically, a Ris object (i.e., an instance of Ris) is created
by specifying its control term (an object of type LVar or Pair), its domain (an
object of type LSet), its lter (an object of type Constraint), and its pattern
(an object of type LVar or Pair). The pattern can be omitted if it coincides with
Example 7 (Ris object creation). The rst RIS of Ex. 2 is created in JSetL as
IntLVar x = new IntLVar();
LSet d = new LSet(new Interval(-2,2));
Constraint f = x.mod(2).eq(0);
Ris ris = new Ris(x,d,f);
// fx:[
Constraint methods provided by Ris implement the constraints = (method LVar and Pair are extended so to accept Ris objects as their arguments. eq) and 6= (method neq). Moreover, the constraint methods in and nin of classes Example 8 (RIS constraints). If ris is the Ris object created in Ex. 7, then the following are possible RIS constraints posted on ris:
LSet s = LSet.empty().ins(2).ins(0).ins(-2);
solver.add(ris.eq(s));
LVar y = new LVar(1);
solver.add(y.nin(ris));
// fx:[
xg = f-2,0,2g
// 1 nin fx:[
The class Ris provides also a number of general utility methods, such as isBound(), which returns true i the domain of the Ris object is bound to some value, and expand which returns the LSet object representing the extensional set denoted by the Ris object (i.e., it performs set grouping) or it raises an exception if the domain of the Ris object is not a completely speci ed set. Example 9. If ris is the Ris object created in Ex. 7, then the corresponding extensional set S is computed and printed as follows:
LSet S = ris.expand().setName("S");
S.output(); whose execution yields S = f2,0,-2g. tu
In JSetL the language of RIS and the language of the parameter theory X are completely amalgamated. Thus, it is possible to use constraints of the latter together with constraints of the former, as well as to share logical variables of both. The following in an example that uses this feature to prove a general property about sets.
Example 10. Check the property of set intersection as stated by the second formula of Ex. 1.
LSet A = new LSet(), B = new LSet(), C = new LSet(); solver.add(C.inters(A,B)); // the constraint C = A \ B LVar X = new LVar(); Ris S = new Ris(X,A,X.in(B)); solver.add(S.neq(C)); // S = fX:A j X 2 Bg // the constraint S 6= C Calling solver.solve() causes an exception Failure to be thrown (i.e., the formula is found to be false). tu
Observe that constraints in JSetL are predicates, not functions; hence we write, for instance, C.inters(A,B), instead of C.eq(A.inters(B)), to denote the predicate inters(A; B; C) which is true i C = A \ B. 5
Intensional set de nition represents a powerful tool for supporting a declarative
programming style, as pointed out for instance in [
A rst interesting application of RIS to support declarative programming is to represent Restricted Universal Quanti ers (RUQ). The RUQ 8x 2 D : F [x] can be easily represented by using a RIS term as follows: D = fx : D j F [x]g: Solving this formula amounts to check whether F [x] holds for all x in D. For instance, D = f1; 2; 3g ^ D = fx : D j x > 0g is true, whereas D = f1; 2; 3g ^ D = fx : D j x > 0g is false.
Since the LRIS solver can decide satis ability of such formulas, then we have a decision procedure for a fragment of rst-order logic with quanti ers.
The following are Java programs that solve simple|though not trivial| problems using JSetL with RIS. Basically, their solution is expressed declaratively as a formula using RUQ.
Example 11. Compute and print the minimum of a set of integers S. public static LVar minValue(LSet S)} throws Failure {
IntLVar x = new IntLVar(); IntLVar y = new IntLVar(); Ris ris = new Ris(x,S,y.le(x)); solver.add(y.in(S).and(S.eq(ris))); solver.solve(); return y; } The method minValue posts the constraint y 2 S ^ S = fx : S j y xg. The solver, non-deterministically binds a value from S to y and then it checks if the property y x is true for all elements x in S. If this is not the case, the solver backtracks and tries a di erent choice for y. A possible call to this method is: Integer[] sampleSetElems = {8,4,6,2,10,5}; LSet R = LSet.empty().insAll(sampleSetElems); LVar min = minValue(R).setName("min"); min.output(); and the printed answer is min = 2.
It is important to observe that operations on RIS are dealt with as real constraints. This implies, among other things, that the order in which constraints are posted to the solver is irrelevant.
More generally, the use of constraints allows to compute with only partial
speci ed aggregates [
Another example that shows the use of RIS to de ne a universal quanti cation in a declarative way is the following simple instance of the well-known map coloring problem.
Example 12. Given a cartographic map of n regions r1,. . . ,rn and a set fc1; : : : ; cmg of colors nd an assignment of colors to the regions such that no two neighboring regions have the same color.
Each region can be represented as a distinct logical variable and a map as a set of unordered pairs (hence, sets) of variables representing neighboring regions. An assignment of colors to regions is represented by an assignment of values (i.e., the colors) to the logical variables representing the di erent regions. public static void coloring(LSet regions, LSet map, LSet colors) throws Failure { solver.add(regions.subset(colors)); LSet p = new LSet(); Ris ris = new Ris(p, map, p.size(2)); solver.add(map.eq(ris)); solver.solve(); } tu The method coloring posts the constraint regions colors ^ map = fp : map j jpj = 2g. The rst conjunct exploits the subset constraint to nondeterministically assign a value to all variables in regions. The second conjunct requires that all pairs of regions in the map have cardinality equal to 2, i.e., all pairs have distinct components. If coloring is called with regions = fr1,r2,r3g, r1, r2, r3 uninitialized logical variables, map = ffr1,r2g,fr2,r3gg, and colors = f"red", "blue"g, the invocation terminates with success, and r1, r2, r3 are bound to "red", "blue", "red", respectively (actually, also the other solution which binds r1, r2, r3 to "blue", "red", "blue", respectively, can be computed through backtracking).
This example uses a pure \generate & test" approach; hence it quickly becomes very ine cient as soon as the map becomes more and more complex. However, it may represent a rst \prototype" whose implementation can be subsequently re ned (e.g., by modeling the coloring problem in terms of Finite Domain (FD) constraints and using the more e cient FD solver provided by JSetL), without having to change its usage. On the other hand, this solution allows to exploit the exible use of constraints and partially speci ed sets. As a matter of fact, the same program can be used to solve related problems; e.g., given a map and a partially speci ed set of colors, nd which constraints the unknown colors must obey in order to obtain an admissible coloring of the map.
The next program shows another example where RIS are used to check whether a property holds for all elements of a set, but using a di erent kind of equality constraint.
Example 13. Check whether n is a prime number or not:4 public static Boolean isPrime(int n)} { if (n <= 0) return false; IntLVar N = new IntLVar(n); IntLVar x = new IntLVar(); LSet D = new LSet(new Interval(2,n/2)); Ris ris = new Ris(x,D,N.mod(x).eq(0)); solver.add(ris.eq(LSet.empty())); return solver.check(); } tu tu The method isPrime posts the constraint fx : [2; N div 2] j N mod x = 0g = ;. The equality between the RIS term and the empty set ensures that there is no x in the interval [2; N div 2] such that N mod x = 0 holds. If, for instance, n is 101, then the call to isPrime returns true. 6
Another important application of RIS is to de ne (partial) functions by giving their domains and the expressions that de ne them. In general, a RIS term of 4 s.check() di ers from s.solve() in that the latter raises an exception if the constraint in the constraint store of s is unsatis able, whereas the former returns a boolean value indicating whether the constraint is satis able or not. the form fx : D j F (x; f (x))g, where f is any function symbol belonging to the language LX , de nes a partial function. In fact, this RIS term denotes a set of ordered pairs as its pattern is an ordered pair; besides, it is a partial function because each of its rst components never appears twice, since they belong to the set D.
Given that RIS are sets, then, in LRIS , functions are sets. Therefore, through standard set operators, functions can be evaluated, compared and point-wise composed; and by means of constraint solving, the inverse of a function can also be computed. The following examples illustrate these ideas in the context of Java with JSetL.
Example 14. The square of an integer n.
IntLVar x = new IntLVar(); LSet D = new LSet();
Ris Sqr = new Ris(x,D,Constraint.TRUE,new Pair(x,x.mul(x)); The Ris object Sqr de nes the set of all pairs (x; x x), where x belongs to an (unknown) set D. This function can be \evaluated" in a point n, and the result sent to the standard output, by executing the following code:
IntLVar y = new IntLVar("y"); solver.solve(new Pair(n,y).in(Sqr)); y.output(); that is, y is the image of n through function Sqr. If, for instance, n has value 5 (e.g., int n = 5), then the printed result is y = 25. Note that the RIS domain, D, is left underspeci ed as a variable. If, for instance, n has value 25, the computed result is y = unknown - Domain: f-5,5g, stating that the possible values for y are -5 and 5.
The interesting aspect of using RIS for de ning functions is that RIS are sets and sets are data. Thus, we have a simple way to deal with functions as data. In particular, since Ris objects can be passed as arguments to a function, we can use RIS to write generic functions that take other functions as their arguments. The following is an example illustrating this technique.
Example 15. The following method takes as its arguments an array of integers A and a function f(x) and updates A by applying f to all its elements. public static void mapList(int[] A,Ris f) throws Failure { for(int i=0; i<A.length; i++) {
IntLVar y = new IntLVar(); solver.solve(new Pair(A[i],y).in(f));
A[i] = y.getValue(); } } If, for instance, the array passed to mapList is f3,5,7g and f is the Ris object Sqr of Ex. 14, then the modi ed array is f9,25,49g. tu
To guarantee that the constraint solver is indeed a decision procedure a number
of restrictions are imposed on the form of RIS in [
Although compliance with these restrictions is important from a theoretical
point of view, in practice there are many cases in which they can be (partially)
relaxed without compromising the correct behavior of programs using RIS.
As noted in [
Unfortunately, the property for a term to be a bijective pattern cannot be
easily syntactically assessed. Thus in [
If the expression used in the RIS pattern de nes a bijective function (e.g., x.sum(2)) then dealing with the RIS is anyway safe; otherwise, it is not safe in general, but it may work correctly in many cases.
Example 16. Compute the set of squares of all even number in [
IntLVar x = new IntLVar(); //ris = fx:[
Allowing more general forms of patterns (and, possibly, control terms) is planned as a future extension for RIS in general, and for the implementation of RIS in JSetL, as well. 5 Note that, on the contrary, a formula such as X = fD[X] j g is an admissible constraint, and it is suitably handled by the LRIS decision procedure. Allowing local variables in RIS raises major problems when the formula representing the RIS lter has to be negated during RIS constraint solving (basically, negation of the RIS lter is necessary to assure that any element that does not satisfy the lter does not belong to the RIS itself). In fact, this would require that the solver is able to deal with quite complex universally quanti ed formulas, which is usually not the case (surely, it is not the case for the JSetL solver). Thus, to avoid such problems a priori, the RIS lter cannot contain local variables.
However, as already observed for RIS patterns, in practice there are cases in which we can relax some restrictions on RIS without losing the ability to correctly deal with such more general RIS constraints.
Thus, in JSetL, we allow the user to specify that some (logical) variables in the RIS lter are indeed local variables. This is achieved|as a temporary solution|by using a special syntax for the external name of the logical variable (namely, the name must start with an underscore character).
Example 17. If R is a set of ordered pairs and D is a set, then the subset of R where all the rst components belong to D can be de ned as follows: LSet D = new LSet(); LSet R = new LSet(); LVar x = new LVar(); LVar y = new LVar("_y"); Pair P = new Pair(x,y)
Ris ris = new Ris(x,D,P.in(R),P); If we try to solve the constraint //ris = fx:D j 9y((x,y) 2 R (x,y))g solver.solve(new Pair(1,2).in(ris).and(new Pair(3,4).in(ris))) i.e., (1; 2) 2 ris ^ (3; 4) 2 ris, then the solver terminates with success, binding (as its rst solution) D to f1; 3 t N1g and R to f(1; 2); (3; 4) t N2g, N1, N2 new fresh variables. tu
In the above example, y is a local variable. If y is not declared as local, then the same call to solver.solve will terminate with failure, since y is dealt with as a free variable and the rst constraint, (1; 2) 2 ris, binds y to 2 so that the second constraint (3; 4) 2 ris fails.
Anyway, it can be observed that many uses of local variables can be avoided by a proper use of the control term and pattern of RIS. For example, the extended RIS of Ex. 17 can be replaced by a RIS term without local variables as follows: f(x; y) : R j x 2 Dg. Hence, the planned extension of the admissible control terms and patterns for RIS can also be useful to alleviate the problem of local variables in RIS lters.
Fact = f(0; 1) t Fact 1g^ Fact 1 = fx : D (2) The class Ris extends the class LSet; hence it is possible, at least in principle, to use Ris objects inside the RIS lter formula in place of LSet objects. This allows, among other things, to de ne recursive restricted intensional sets (RRIS).
Of course, the presence of recursive de nitions may compromise the niteness of RIS and hence the decidability of the formulas involving them. Therefore RRIS are prohibited in the base language of RIS, LRIS . In practice, however, their availability can considerably enhance the expressive power of the language and hence RRIS are allowed in the extended language supported by JSetL. Programmers are responsible of guaranteeing termination.
The following is an example using a RRIS. Since RRIS has not yet been fully developed and tested in JSetL we will write programs dealing with them by using only the abstract notation.
j 9y; z(x > 0 ^ (x
1; z) 2 Fact ^ y = x z (x; y))g Note that the domain, D, is left underspeci ed, and recursion is simply expressed as a set membership predicate over the same set being de ned: (x 1; z) 2 Fact means that z is the factorial of x 1. If we conjoin, for example, the constraint (5; f ) 2 Fact then the solver will return f = 120. As usual in declarative programming, there is no real distinction between inputs and outputs. Therefore if we conjoin to formula (2) the constraint (n; 120) 2 Fact then the solver will return n = 5. tu
RRIS are not yet fully supported in JSetL, but their inclusion, which has already been successfully experimented in flogg, should be feasible without major problems. 8
In this paper we have presented an extension of the Java library JSetL to support
RIS, and we have shown, through a number of simple examples, the usefulness
of RIS as a powerful data and control abstraction. Although e ciency is not
our main concern, the implementation of RIS in flogg has proven to be e cient
enough as to compete with mainstream tools [
As future work, it can be interesting: (a) on the more theoretical side, trying to extend the language of RIS for which we are able to provide a correct and complete solver, e.g. by enlarging the collection of set and relation operators dealing with RIS (for now limited to equality and membership); (b) on the more practical side, trying to incorporate in the implementation of RIS within the JSetL library all the extensions mentioned in Sect. 7, which although falling outside of the decision procedure, turn out to be of great interest in practice. Acknowledgments We wish to thank Andrea Guerra and Andrea Fois for their contribution to the implementation of RIS in JSetL. This work has been partially supported by GNCS \Gruppo Nazionale per il Calcolo Scienti co".