A decision procedure for a two-sorted extension of Multi-Level Syllogistic with the Cartesian product and some map constructs Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo Dipartimento di Matematica e Informatica, Università di Catania, Italy {cantone, longo, nicolosi}@dmi.unict.it Abstract. We present a nondeterministic polynomial-time decision pro- cedure for an extension of multi-level syllogistic with the singleton oper- ator, the Cartesian product, various map constructs, and special predi- cates asserting respectively that a map term is single valued, injective, and bijective, but with no map image or domain operators. We also prove that the extension of multi-level syllogistic with a map image operator has an ExpTime-hard decision problem, via a reduction of the decision problem for the description logic ALC. Keywords: Decision procedures, multi-level syllogistics, Cartesian prod- uct, map constructs, NP-completeness, ExpTime-hardness. 1 Introduction The decision problem in set theory has been intensively investigated in the last decades. The initial motivations can be traced back in 1978, when Jack Schwartz1 envisaged an interactive proof checker supposed to accept sequences of logical formulae, such that any formula in the sequence follows logically from earlier formulae (cf. [13]). To keep at a reasonable level the mass of details that a user must key in, he argued that such a system should include among other fun- damental components also an inferential core, comprised of an extensive (and extendible) collection of efficient (semi-)decision procedures to handle elemen- tary inferential steps. Additionally, the language of set theory, which pervades most mathematical reasoning, seemed to be the most appealing one for such an enterprise. Multi-level syllogistic (in short, MLS) has been the first unquantified sublan- guage of set theory to be studied in this context. We recall that MLS involves besides set variables and the ‘null set’ constant ∅, also the common Boolean set operators ∪, ∩, \, the set predicates ∈, ⊆, and =, and the propositional connectives. Over the years, decision procedures or proofs of undecidability have been provided for several extensions of MLS and also for various quantified fragments 1 January 9, 1930 – March 2, 2009. 2 Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo of set theory, contributing to the rise of the field of Computable Set Theory (see [2, 5] for a thorough account of the state-of-the-art until 2001). It is to be noticed, however, that several decision procedures found so far are not practical at all and their interest is limited to the foundational purpose of identifying the boundary between the decidable and the undecidable in set theory. The quite recent implementation of the proof-verification system ÆtnaNova/Referee described in [11, 6, 10] has given a new impulse to the in- vestigation of effective2 decision procedures with the goal of enhancing its infer- ential capabilities. For instance, [3] presents some commonly occurring decidable extensions of MLS. In this paper we present an effective procedure (namely, having a nondeter- ministic polynomial-time complexity) for an extension of MLS with the singleton operator, the Cartesian product, and various map constructs, which we denote MLSS× × 2,m . More specifically, MLSS2,m is a two-sorted language with set and map variables. Set variables range over sets of the von Neumann cumulative hierarchy of sets and map variables range over collections of pairs of sets (this acceptation of the term ‘map’ agrees with the map data structure in the SETL language; see [14]). Since map variables and set variables have different sorts, we do not need to be specific on the internal representation of pairs, as long as the basic property of pairs holds: [x, y] = [x0 , y 0 ] ⇐⇒ x = x0 ∧ y = y 0 . Map terms can be formed by means of the Cartesian product, various map restriction operators, a map inverse operator, and the Boolean set operators on maps. Additionally, the language allows assertions meaning that a map term is single-valued, or injective, or bijective. However, for efficiency reasons, domain and range operators are not allowed, since, as we will show in Section 4, their presence triggers the ExpTime-hardness of the decision problem. A similar two-sorted language, extended with domain and range operators, but with no Cartesian product and no Boolean set operators among map terms, has been considered in [9], but the decision procedure proposed there had a double exponential time complexity. The language in [9] has been subsequently extended with various topological constructs, without disrupting decidability. We mention also a one-sorted version of the language considered in [9], fur- ther extended with map evaluation (cf. [7]). In this case, since there is no dis- tinction between set and map variables, maps (i.e., sets) can be combined with the Boolean set operators as well. However, the language in [7] does not allow a predicate IsMap(x), asserting that x is a collection of pairs. Therefore, for in- stance, a predicate of type Inverse(f, g) expresses only that g is an inverse of f , up to non-pair elements, so that Inverse(f, g) and Inverse(f, g 0 ) do not imply that g = g 0 , but only that g and g 0 contain the same pairs (namely the inverse of 2 Needless to say, any decision procedure for a language at least as expressive as propo- sitional logic has at least a nondeterministic polynomial-time complexity. This is the case for all extensions of MLS. Thus, our meaning of ‘effective’ is just nondetermin- istic polynomial-time. Title Suppressed Due to Excessive Length 3 the pairs contained in f ). Despite the peculiarity of such semantics, the decision procedures given in [7] has a nondeterministic exponential time complexity. The paper is organized as follows. Section 2 gives the precise syntax and semantics of the language MLSS× 2,m of our interest. A decision procedure for × MLSS2,m and its complexity analysis are then reported in Section 3. In Section 4 we prove that the extension of MLS with the image operator has an ExpTime- hard decision problem. Finally, we briefly give some hints to future work in Section 5. 2 The language MLSS× 2,m 2.1 Syntax MLSS×2,m (Multi-Level Syllogistic with singleton, Cartesian product, and various map constructs) is a two-sorted language which contains: (i) a countably infinite collection of set variables Vars s = {x, y, z, . . .}; (ii) a countably infinite collection of map variables Vars m = {f, g, h, . . .}; (iii) the predicate symbols ∈, =, ⊆, injective(·), single valued(·), bijective(·); (iv) the operator symbols ∩, ∪, \, × (Cartesian product), {·} (singleton), (·)·| , (·)|· , (·)·|· (map restriction operators), (·)−1 (map inverse); (v) the constant ∅ (empty set); (vi) parentheses (to construct compound terms); (vii) the logical connectives ¬, ∧, ∨, →, ↔ (to construct compound formulae). MLSS× 2,m -set terms are recursively defined as follows: 1. each set variable and the constant ∅ are set terms; 2. if X, Y are set terms, then so are X ∪ Y , X ∩ Y , X \ Y , {X}. MLSS× 2,m -map terms are recursively defined as follows: 1. each map variable is a map term; 2. if X, Y are set terms and F, G are map terms then – X ×Y, – FX| , F|Y , FX|Y (left, right, and left-right restriction, respectively), – F −1 , F ∪ G, F ∩ G, F \ G are map terms. MLSS× 2,m -atomic formulae are defined from set terms and map terms in the following way. Let X, Y be set terms and F, G be map terms, then 1. X ∈ Y , X ⊆ Y , X = Y , 2. [X, Y ] ∈ F , F ⊆ G, F = G, 3. injective(F ), single valued(F ), bijective(F ) 4 Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo are atomic formulae. Observe that a formula of type [X, Y ] ∈ F is to be con- sidered just as a ternary relationship among X, Y , and F , since we did not introduce any set term of type [X, Y ]. Then the set of MLSS× 2,m -formulae is the smallest set containing all the × MLSS2,m -atomic formulae and that is closed with respect to the logical con- nectives ¬, ∧, ∨, →, ↔. Usually, to denote MLSS× 2,m -formulae we will use the metavariables ϕ and ψ. For an MLSS× 2,m -formula ϕ, we denote by Vars s (ϕ) and Vars m (ϕ) the col- lections of set variables and of map variables occurring in ϕ, respectively, and we put Vars(ϕ) = Def Vars s (ϕ) ∪ Vars m (ϕ). 2.2 Semantics The semantics of MLSS× 2,m is based upon the von Neumann standard cumulative hierarchy V of sets defined by: V0 = ∅ Vγ+1 = P(V S γ) , for each ordinal γ Vλ = µ<λ Vµ , for each limit ordinal λ S V = γ∈On Vγ , where, given a set S, P(S) is the power set of S, and On indicates the class of all ordinals. It can be proved that the membership relation is well-founded in V and, therefore, no membership cycle can occur in V. We denote with rank(u) the least ordinal γ such that u ⊆ Vγ (i.e., u ∈ Vγ+1 ), for every set u in V. An assignment is a total function M : Vars s ∪ Vars m −→ V that maps each set and map variable into a set of the von Neumann hierarchy V, such that M f is a set of ordered pairs, for any f ∈ Vars m . It is not relevant which representation is chosen for ordered pairs, as long as the basic ordered pair property holds. One possibility could be to adopt Kuratowski’s definition and put [u, v] = Def {{u}, {u, v}}, for all sets u and v. An assignment M is said to be injective with respect to a set of variables S ⊆ Vars s , if M x 6= M y, for all distinct variables x, y in S. Assignments extend naturally to set terms and map terms. For instance, we have: M (X × Y ) = {[u, v] : u ∈ M X ∧ v ∈ M Y } , M FX| = {[u, v] : [u, v] ∈ M F ∧ u ∈ M X} , M F|Y = {[u, v] : [u, v] ∈ M F ∧ v ∈ M Y } , M FX|Y = {[u, v] : [u, v] ∈ M F ∧ u ∈ M X ∧ v ∈ M Y } , where X, Y are set terms and F is a map term.3 3 For simplicity, in the following we will use the same operator and predicate symbols also at the semantic level. So, for instance, for any map m and set s, ms| will denote the map {[u, v] : [u, v] ∈ m ∧ u ∈ s}. This will generate no confusion. Title Suppressed Due to Excessive Length 5 Assignments evaluate atomic formulae of type X ∈ Y , X ⊆ Y , X = Y , F ⊆ G, and F = G, to a truth value true or false in the standard way. Atomic formulae of the other types are evaluated as follows: M ([X, Y ] ∈ F ) is true ⇐⇒ [M X, M Y ] ∈ M F, M (single valued(F )) is true ⇐⇒ (∀u, v, v 0 )({[u, v], [u, v 0 ]} ⊆ M F → v = v 0 ), M (injective(F )) is true ⇐⇒ (∀u, u0 , v)({[u, v], [u0 , v]} ⊆ M F → u = u0 ), M (bijective(F )) is true ⇐⇒ (∀u, v, u0 , v 0 )({[u, v], [u0 , v 0 ]} ⊆ M F → (u = u0 ↔ v = v 0 )). Finally, evaluation of compound formulae by an assignment M follows the stan- dard rules of propositional logic. Let M be an assignment and ϕ a formula of MLSS× 2,m . We say that M satisfies ϕ (and write M |= ϕ) if M evaluates ϕ to true. In this case M is said to be a model for ϕ. A formula ϕ is satisfiable if there is an assignment that satisfies it. Two formulae ϕ and ψ are equisatisfiable, when ϕ is satisfiable if and only if ψ is also satisfiable. A formula ϕ is injectively satisfiable with respect to a set of variables S if there is an injective assignment with respect to the set of variables S that satisfies it. The satisfiability problem for MLSS× 2,m is then the problem of establishing × for any given formula of MLSS2,m whether it is satisfiable or not. Since the evaluation of an MLSS× 2,m -formula by an assignment depends solely on the values which it assumes over the variables occurring in the formula, in most cases we will deal with partial assignments, though we will refer to them just as ‘assignments’. By way of a simple normalization process of the type described in [2, §3.8], it is easy to show that the satisfiability problem for MLSS× 2,m -formulae reduces × to the satisfiability problem for normalized MLSS2,m -conjunctions, namely con- junctions of MLSS× 4 2,m -literals of the types reported in Table 1. For instance, to see that literals of type single valued(f ) and ¬single valued(f ) can be dismissed, it is enough to observe that ¬single valued(f ) is equisatisfiable with [x, y] ∈ f ∧ [x, y 0 ] ∈ f ∧ y ∈ z ∧ y 0 ∈ / z, where x, y, y 0 , z are newly introduced set variables, and that single valued(f ) is equivalent to injective(f −1 ), which in turn is equisatisfiable with g = f −1 ∧ injective(g), where g is a newly introduced map variable. 3 A decision procedure In this section we describe a nondeterministic polynomial-time decision proce- dure for the satisfiability problem for normalized MLSS×2,m -conjunctions. The key idea behind such procedure is that a normalized MLSS× 2,m -conjunction is 4 Plainly, the expressions x ∈ / y and [x, y] ∈/ f in Table 1 are shorthands for the literals ¬(x ∈ y) and ¬([x, y] ∈ f ), respectively. 6 Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo x∈y x∈ /y [x, y] ∈ f [x, y] ∈ /f y = {x} x=y∪z x=y\z f =g∪h f =g\h f =x×y g = fx| g = f −1 injective(f ) Table 1. Literals in normalized MLSS× 2,m -conjunctions. satisfiable if and only if there exists a finite structure, to be introduced later, which witnesses this fact, in a sense that will be clarified below. In addition, the total size of such structure has a bound depending solely on the size of the conjunction, This decision procedure is a generalization of the one presented in [1] for the extension MLSS of MLS with a singleton operator. To begin with, it is convenient to introduce some notations and definitions. Given a relation % over a set N and a nonempty subset V ⊆ N , we say that 6 h % a0 i, for all distinct a, a0 ∈ V , where % is V -extensional if h % ai = h % ai = Def {b ∈ N : b % a} . Next, let ∈ b be an acyclic relation over a finite set N and let V ⊆ N . We introduce a notion of height relative to V , for x ∈ V , with the following recursion:  0 if y ∈ / x, with y ∈ V , b V -height(x) =  max V -height(y) : y ∈ V ∧ y ∈ b x + 1 otherwise. We will use MLSS×2,m -relation systems to witness the satisfiability of normal- ized MLSS×2,m -conjunctions. These are defined as follows. Definition 1 (MLSS× 2,m -relation system). An MLSS× 2,m -relation system is a   tuple G = V, T, F, ∈, {f : f ∈ F } , where b b – V and T are finite disjoint collections of set variables such that V 6= ∅, – F is a finite collection of map variables, ∈ – n o relation over V ∪ T , b is an acyclic – f : f ∈ F is a collection of relations over V ∪ T . b t u MLSS× 2,m -relation systems allow to define special assignments, which are called realizations. Definition 2 (Realization of an MLSS×2,m -relation system).   Let G = V, T, F, ∈, {f : f ∈ F } be an MLSS× -relation system and let b b 2,m {ut : t ∈ T } be a collection of sets. Then the realization of G relative to {ut : t ∈ T } is the assignment R over (V ∪ T ) ∪ F defined recursively by: Title Suppressed Due to Excessive Length 7  R x = R z : z ∈ bx , for x ∈ V , R t = nR z : z ∈ b t ∪ {ut } , o for t ∈ T , R f = [R x, R y] : x fb y, for x, y ∈ V ∪ T , for f ∈ F . t u The following lemma states conditions on MLSS× 2,m -relation systems which guarantee that it has realizations satisfying specific MLSS× 2,m -literals. It will be used later to prove the correctness of the decision procedure outlined in Theorem 1 below.   Lemma 1. Let G = V, T, F, ∈ b , {fb : f ∈ F } be an MLSS× 2,m -relation system and let {ut : t ∈ T } be a collection of sets such that (a) ∈ b is V -extensional; (b) ut 6= ut0 , for all distinct t, t0 ∈ T ; (c) ut 6= R x, for all t ∈ T, x ∈ V ∪ T . Then (i) R is injective w.r.t. V ∪ T (i.e., R x 6= R x0 , for all distinct x, x0 ∈ V ∪ T ); (ii) R x ∈ R x0 ⇐⇒ x ∈ b x0 , for all x, x0 ∈ V ∪ T ; (iii) R x = R y ∪ R z ⇐⇒ h ∈ b xi = h ∈ b yi ∪ h ∈ b zi, for all x, y, z ∈ V ; (iv) R x = R y \ R z ⇐⇒ h ∈ xi = h ∈ yi \ h ∈ zi, for all x, y, z ∈ V ; b b b (v) R x = {R y} ⇐⇒ h ∈ b xi = {y}, for all x ∈ V and y ∈ V ∪ T ; (vi) [R x, R y] ∈ R f ⇐⇒ x fb y, for all x, y ∈ V ∪ T and f ∈ F ; (vii) R f = R x × R y ⇐⇒ fb = h ∈ b xi × h ∈ b yi, for all x, y ∈ V and f ∈ F ; (viii) R f = (R g)R x| ⇐⇒ fb = (b g )h ∈b xi| , for all x ∈ V and f, g ∈ F ; (ix) R f = R g ∪ R h ⇐⇒ fb = gb ∪ b h, for all f, g, h ∈ F ; (x) R f = R g \ R h ⇐⇒ fb = gb \ b h, for all f, g, h ∈ F ; (xi) R f = (R g)−1 ⇐⇒ fb = (b g )−1 , for all f, g ∈ F ; (xii) injective(R f ) ⇐⇒ injective(fb), for every f ∈ F . Proof. (i) To prove that R is injective with respect to V ∪ T we reason as follows. Let x, x0 be two distinct set variables in V ∪ T . We have to prove that R x 6= R x0 . To begin with, let us assume that {x, x0 } ∩ T 6= ∅, and let, without loss of generality, x ∈ T . If R x = R x0 , then ux ∈ R x0 , which by (c) implies ux = ux0 , contradicting (b). Thus R x 6= R x0 . Instead, if x, x0 ∈ V , we proceed by induction on µ = max(V -height(x), V -height(x0 )). In the base case µ = 0, by V -extensionality, there must exist a t ∈ T such that t ∈ / 0. b x if and only if t∈x b Suppose, without loss of generality, that t ∈ / 0 . Thus R t ∈ R x \ R x0 . b x and t∈x b Indeed, if R t ∈ R x0 , then there exists y ∈ V ∪T such that y ∈ b x0 and R t = R y. But then, as in the previous case, we would have that t and y have to be identical and therefore t ∈ b x0 , which is a contradiction. Thus R x 6= R x0 . For the inductive step, suppose by contradiction that R x = R x0 , whereas (i) is true for every distinct y, y 0 ∈ V such that max(V -height(y), V -height(y 0 )) < max(V -height(x), V -height(x0 )) . (1) 8 Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo By V -extensionality, since x and x0 are distinct, there must be a y ∈ V ∪ T such that y ∈ / 0 . Suppose, without loss of generality, that y ∈ b x if and only if y ∈x b b x 0 0 0 0 b 0 and y ∈x / . Since R x = R x , there must be a y ∈ V ∪ T such that y ∈ x and b R y = R y 0 . But then, from the base case if {y, y 0 } ∩ T 6= ∅, or from the inductive hypothesis if y, y 0 ∈ V , y and y 0 must be identical. This implies that w ∈ b v0 , a contradiction. Thus we have R x 6= R x even if x, x ∈ V , whenever x and x0 0 0 are distinct. Next we prove (ii). Plainly, if x ∈ b x0 then R x ∈ R x0 . On the other hand, 0 b x0 and if R x ∈ R x , then by (c) there must exist a y ∈ V ∪ T such that y ∈ R x = R y. But then, by (i), x and y must coincide and therefore x ∈ b x0 . In order to prove (iii), let x, y, z ∈ V and assume first that R x = R y ∪ R z. Then for every x0 ∈ V ∪ T we have: x0 ∈ h ∈ b xi ⇐⇒ R x0 ∈ R x ⇐⇒ R x0 ∈ R y ∪ R z ⇐⇒ R x ∈ R y or R x ∈ R z ⇐⇒ x0 ∈ h ∈ 0 0 b yi or x0 ∈ h ∈ b zi ⇐⇒ 0 x ∈h ∈ b yi ∪ h ∈ b zi, so that h ∈ b xi = h ∈ b yi ∪ h ∈b zi. Analogously one can prove that h ∈ b xi = h ∈b yi ∪ h ∈ b zi implies R x = R y ∪ R z. Properties (iv) and (v) can be proved much as (iii). (vi) follows immediately the very definition of R f and from the injectivity of the realization R w.r.t. V ∪ T , already proved in (i). To prove (vii), let f ∈ F , x, y ∈ V and suppose initially that R f = R x×R y. Let x0 , y 0 be such that x0 fb y 0 . Then, by Definition 2, [R x0 , R y 0 ] ∈ R f , so that R x0 ∈ R x and R y 0 ∈ R y. Thus, (ii) yields x0 ∈ b x and y 0 ∈ b y, and therefore fb ⊆ h ∈ b xi×h ∈ b yi. Similarly, it can be shown that h ∈ b xi×h ∈ b yi ⊆ fb, which together with the previous inclusion implies fb = h ∈ b xi × h ∈ b yi. Conversely, assume that fb = h ∈ b xi × h ∈ b yi. By (i), (vi), and Definition 2, [u, v] ∈ Rf holds if and only if there are x0 , y 0 ∈ V ∪ T such that R x0 = u, R y 0 = v, and x0 fb y 0 . From our assumption, it follows that x0 ∈ b x and y 0 ∈ b y. Thus, by (ii), we have that u ∈ R x and v ∈ R y, so that R f ⊆ R x × R y. To show that R x × R y ⊆ R f , let [u, v] ∈ R x × R y. Since x, y ∈ V , there exist x0 , y 0 in V ∪ T such that R x0 = u, R y 0 = v, x0 ∈ b x, and y 0 ∈ b y. Hence, by our assumption, 0 b 0 x f y , and therefore [u, v] ∈ R f , proving that R x × R y ⊆ R f . To prove (viii), assume first that R f = (R g)R x| . Then fb = (b g ) b follows h ∈xi| plainly from (ii) and (vi). Next suppose that fb = (b g )h ∈b xi| and let u, v be any two sets such that [u, v] ∈ R f . Then there exist x0 , y 0 in V ∪ T such that R x0 = u, R y 0 = v, and x0 fb y 0 . But then, since fb = (b g )h ∈b xi| , we have x0 gbv 0 , and x0 ∈ b x, so that [u, v] ∈ R g and u ∈ R x, which in turn implies [u, v] ∈ (R g)R x| , and therefore R f ⊆ (R g)R x| . The converse inclusion can be proved analogously, completing the proof of (viii). Properties (ix), (x), and (xi) are direct consequences of (vi). Finally, let us prove (xii). First suppose that R f is injective and let x, y, y 0 ∈ V ∪ T such that x fb y and x fb y 0 . By (vi), [R x, R y] and [R x, R y 0 ] are in R f . Thus, by the assumed injectivity of R f and by (i), it follows that y = y 0 , proving that the map fb is injective. Conversely, let us assume that fb is injective. If [u, v] and [u, v 0 ] are in R f , then there must exist x, y, y 0 in V ∪ T such that R x = u, Title Suppressed Due to Excessive Length 9 R y = v, R y 0 = v 0 , x fb y, and x fb y 0 . The injectivity of fb implies y = y 0 , so that v = R y = R y 0 = v 0 , proving that R f is injective too. t u To any given assignment M and given collections of set and map variables, it is possible to associate a particular MLSS× 2,m -relation system, called canonical, which represents all membership relations among pairs of sets (M x, M y) and pairs of type ([M x, M y], M f ), where x, y are set variables and f is a map variable belonging to the given collections of variables. Definition 3 (Canonical MLSS× 2,m -relation system). Given – two disjoint finite collections V and T of set variables, such that V 6= ∅, – a finite collection F of map variables, – an assignment M over (V ∪ T ) ∪ F , injective with respect to the variables in V ∪ T, then the canonical MLSS×2,m -relation system G M of M relative to (V, T, F ) is the × MLSS2,m -relation system (cf. Definition 1)   G M = Def V, T, F, ∈b M, {fbM: f ∈ F } , where – x∈b M y ⇐⇒ M x ∈ M y, for every x, y ∈ V ∪ T , – x fbM y ⇐⇒ [M x, M y] ∈ M f , for every x, y ∈ V ∪ T and f ∈ F . t u The following lemma states some properties of canonical MLSS× 2,m -relation systems which will be used to prove the completeness of the decision procedure given in Theorem 1.   Lemma 2. Let V , T , F , M , and G M = V, T, F, ∈ b M, {fbM: f ∈ F } be as in Definition 3. Then, the following properties hold: b M is acyclic; (i) ∈ (ii) if M x ∈ M y then x ∈b M y, for x, y ∈ V ∪ T ; (iii) if M x ∈ / M y then ¬(x ∈ b M y), for x, y ∈ V ∪ T ; (iv) if M x = M y ∪ M z then h ∈ b xi = h ∈ b yi ∪ h ∈ b zi, for x, y, z ∈ V ∪ T ; (v) if M x = M y \ M z then h ∈ b M xi = h ∈ b M yi \ h ∈ b M zi, for x, y, z ∈ V ; M (vi) if M x = {M y} then h ∈ b xi = {y}, for x, y ∈ V ∪ T ; (vii) if [M x, M y] ∈ M f then x fbM y, for x, y ∈ V ∪ T and f ∈ F ; / M f then ¬(x fbM y), for x, y ∈ V ∪ T and f ∈ F ; (viii) if [M x, M y] ∈ (ix) if M f = M x × M y then fbM = h ∈ b M xi × h ∈ b M yi, for x, y ∈ V ∪ T and f ∈ F; (x) if M f = (M g)M x| then fbM = (b g M )h ∈b Mxi| , for f ∈ F and x ∈ V ; (xi) if M f = M g ∪ M h then fbM = gbM ∪ b hM , for f, g, h ∈ F ; M M (xii) if M f = M g \ M h then fb = gb \ b hM , for f, g, h ∈ F ; (xiii) if M f = (M g)−1 then fbM = (b g M )−1 , for f, g ∈ F ; 10 Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo (xiv) if injective(M f ) then injective(fbM ), for f ∈ F . b M and the acyclicity of the Proof. (i) plainly follows from the definition of ∈ membership relation on sets. The remaining statements are immediate conse- quences of Definition 3. t u The decidability of the satisfiability problem for normalized MLSS× 2,m - conjunctions is proved in the following theorem. Theorem 1. Let ϕ be a normalized MLSS× 2,m -conjunction, V = Vars s (ϕ), and F = Vars m (ϕ). Then ϕ is injectively satisfiable w.r.t. V if and only if there exist: – a finite collection T = {t1 , . . . , tm } of set variables, disjoint from V , with m = |T | ≤ |V | − 1,   – an MLSS× 2,m -relation system G = V, T, F, ∈ b , { b: f ∈ F} f such that (a) ∈b is V -extensional; (b) if x ∈ y occurs in ϕ then x ∈ b y, for x, y ∈ V ; (c) if x ∈ / y occurs in ϕ then x ∈ b/ y, for x, y ∈ V ; (d) if [x, y] ∈ f occurs in ϕ then x fb y, for x, y ∈ V, f ∈ F ; (e) if [x, y] ∈/ f occurs in ϕ then [x, y] ∈ / fb, for x, y ∈ V, f ∈ F ; (f ) if x = y ∪ z occurs in ϕ then h ∈ xi = h ∈ b b yi ∪ h ∈ b zi, for x, y, z ∈ V ; (g) if x = y \ z occurs in ϕ then h ∈ xi = h ∈ yi \ h ∈ zi, for x, y, z ∈ V ; b b b (h) if f = g ∪ h occurs in ϕ then fb = gb ∪ b h, for f, g, h ∈ F ; (i) if f = g \ h occurs in ϕ then fb = gb \ b h, for every f, g, h ∈ F ; (j) if f = x × y occurs in ϕ then fb = h ∈ b xi × h ∈ b yi, for x, y ∈ V , f ∈ F ; (k) if f = gx| occurs in ϕ then f = fh ∈b xi| , for x ∈ V , f ∈ F ; b b (l) if injective(f ) occurs in ϕ then fb is injective, for every x ∈ V , f ∈ F ; Proof. We show first that the conditions of the theorem are sufficient for ϕ to  be injectively satisfiable  w.r.t. V . Thus, let T = {t1 , . . . , tm } and G = V, T, F, ∈ b , {fb : f ∈ F } be as in the hypotheses and such that (a)–(l) hold. We use Lemma 1 to prove that some realization of the MLSS× 2,m -relation system G is an injective model for ϕ w.r.t. V . To this end, it is enough to exhibit a collection of sets {uti : ti ∈ T } such that (A) uti 6= utj , for all distinct ti , tj ∈ T , and (B) uti 6= R x, for all ti , ∈ T and v ∈ V ∪ T , where R is the realization of G relative to {uti : ti ∈ T } and (V, T ). Let us put uti = Def {n, i}, for ti ∈ T , where n = |V |.5 The sets uti are obviously pairwise 5 We are assuming the von Neumann representation of natural numbers 0 = Def ∅, 1 = Def {0}, 2 = Def {0, 1}, and so on. Title Suppressed Due to Excessive Length 11 distinct. In addition, we have rank(uti ) = n + 1, for uti ∈ T . Hence, to prove (B), we can just show that rank(R x) 6= n + 1, for each x ∈ V ∪ T . Thus, let x ∈ V ∪ T . If uti ∈+ R x (where ∈+ denotes the transitive closure of the + membership relation) then rank(R v) > n + 1. On the other hand, if uti ∈ / Rx for all uti ∈ T , by induction on V -height(x) it follows that rank(R x) < n. Properties (b)–(l) and Lemma 1 guarantee that R satisfies all literals in ϕ. For instance, if the literal x ∈ y occurs in ϕ, then by (b) we have x ∈ b y, so that Lemma 1(ii) yields R x ∈ R y. Reasoning in a similar way, one can show that R satisfies all the conjuncts in ϕ. Additionally, by Lemma 1(i), R is injective w.r.t. V ∪ T , completing the proof of the sufficiency part of the theorem. Conversely, let M be a model for ϕ which is injective w.r.t. the collection of variables V = Vars s (ϕ). We show next how to construct a collection T = {t1 , . . . , tm } of set variables with m = |T | ≤ |V | − 1, and an MLSS× 2,m -relation   system G = V, T, F, ∈ b , {fb : f ∈ F } such that conditions (a)–(l) of Lemma 1 are satisfied. It is convenient to introduce the following notion (cf. [1]). We say that a set Σ distinguishes a set S if s ∩ Σ 6= s0 ∩ Σ holds for any two distinct s, s0 ∈ S. Claim.6 Any finite set S admits a set Σ which distinguishes it and such that |Σ| ≤ |S| − 1. Proof. If |S| ≤ 1, our claim is vacuously true. Otherwise, let |S| > 1 and, inductively, let us assume that our claim holds for any set S 0 such that |S 0 | < |S|. Then, pick s ∈ S. By our inductive hypothesis the set S \ {s} admits a set Σ 0 which distinguishes it and such that |Σ 0 | ≤ |S| − 2. If Σ 0 distinguishes S, we are done. Otherwise, there is an s0 ∈ S \ {s} such that s ∩ Σ 0 = s0 ∩ Σ 0 . Let d ∈ (s\s0 )∪(s0 \s) and consider Σ = Def Σ 0 ∪{d}. We assert that Σ distinguishes S. Indeed, if this were not the case there would exist an s00 ∈ S \ {s, s0 } such that s ∩ Σ = s00 ∩ Σ, so that s ∩ Σ 0 = s00 ∩ Σ 0 and, therefore, s0 ∩ Σ 0 = s00 ∩ Σ 0 , contradicting our assumption that Σ 0 distinguishes S \ {s}. It only remains to observe that |Σ| ≤ |S| − 1. t u In view of the above claim, let Σ M be a set which distinguishes {M x : x ∈ V } and is such that |ΣM | ≤ |V | − 1. Also, let m = |Σ M \ {M x : x ∈ V }| ≤ |V | − 1 and let T = {t1 , . . . , tm } be a collection of m distinct set variables not belonging to V . Let us extend/redefine M over the variables  in T in such a way that  M M b M, {fbM : f ∈ F } {M ti : ti ∈ T } = Σ \{M x : x ∈ V } and let G = V, T, F, ∈ be the canonical MLSS× 2,m -relation system of M relative to (V, T ) and F . From the well-foundedness of the membership relation in V, we have immediately that b M is acyclic. Additionally, by construction, if x, x0 ∈ V are any two distinct ∈ variables, then there exists y ∈ V ∪T such that M y ∈ ((M x\M x0 )∪(M x0 \M x)). Hence y ∈ b M x ⇐⇒ y ∈ / M x0 , proving the V -extensionality of ∈ b b M (condition (a)). Conditions (b)–(l) follows from Lemma 2 and from the fact that M satisfies all the literals of ϕ. For instance, if x ∈ y occurs in ϕ, then we have plainly 6 See [1]. [12] also provides an extension to infinite sets. 12 Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo M x ∈ M y. Thus, by Lemma 2(ii), we have x ∈ b M y. The remaining conditions can be proved much in the same way, concluding the proof that the conditions of the theorem are also necessary for the injective satisfiability of ϕ w.r.t. V . t u Since an MLSS× 2,m -conjunction ψ of literals of the types listed in Table 1 is satisfiable if and only if there exists an equivalence relation ∼ on Vars s (ψ) e where ψe is the MLSS× - such that ψe is injectively satisfiable (w.r.t. Vars s (ψ)), 2,m conjunction obtained from ψ by identifying ∼-equivalent set variables, namely by replacing them by a common representative, we have the following result. Corollary 1. The ordinary satisfiability problem for the class of MLSS× 2,m - formulae is solvable. t u 3.1 Complexity issues Theorem 1 leads to a nondeterministic polynomial-time decision test for the injective satisfiability problem for normalized MLSS× 2,m -conjunctions (w.r.t. the collection of its set variables). Lemma 3. The injective satisfiability problem for normalized MLSS× 2,m - conjunctions w.r.t. set variables is NP-complete. Proof. To begin with, the NP-hardness of the class of formulae of our interest follows immediately from the NP-hardness of MLSS (cf. [4]). Concerning its membership to NP, we reason as follows. Let ϕ be a normalized MLSS× 2,m - conjunction which admits an injective model, relative to its set variables. This fact can be witnessed by the existence of an MLSS× 2,m -relation system   G = Vars s (ϕ), T, Vars m (ϕ), ∈ b , {fb : f ∈ Vars m (ϕ)} , with |T | < |Vars s (ϕ)|, such that conditions (a)–(l) of Theorem 1 are satisfied. Since the size of G is at most quadratic in the size of ϕ and since conditions (a)– (l) can be verified in polynomial-time, it follows that the injective satisfiability problem for normalized MLSS× 2,m -conjunctions is in NP and, therefore, is NP- complete. t u In view of Corollary 1 and the remarks just before its statement, we have also the NP-completeness of the ordinary satisfiability problem for normalized MLSS× 2,m -conjunctions. To this end, it is enough to observe that given an equiv- alence relation ∼ on the set variables of a normalized MLSS× 2,m -conjunction ϕ, then ϕe can be computed in linear time (obviously, relative to the size of ϕ). Thus we have: Corollary 2. The ordinary satisfiability problem for normalized MLSS× 2,m - conjunctions is NP-complete. Title Suppressed Due to Excessive Length 13 3.2 Remarks on the domain and image operators The same approach of Theorem 1 can not readily be applied to deal also with the extension of MLSS×2,m with literals of the type x = dom(f ), where the semantics of the dom(·) operator is the obvious one, namely M (dom(f )) = Def {s : [s, u] ∈ M f, for some set u} , for any assignment M . Consider for instance a formula ϕ containing  the literals x = dom(f  0 ) and M M M y ∈ x and let M be a model for ϕ. Let G = V, T, F, ∈ b , {f : f ∈ F } be the b canonical MLSS× 2,m -relation system of M , relative to a certain set T of auxiliary variables and let us assume that M x = {M y} and M f0 = {[M y, v]}, where v 6= M z for every set variable z ∈ V ∪ T . Then fb0M= ∅ and ∅ = dom(fb0M) 6= h ∈ b xi = {y} . Most likely, any extension of the decision test contained in Theorem 1 to deal also with literals of type x = dom(f ) will involve the introduction in T of ex- ponentially many auxiliary set variables in the size of the input formula. This is supported by the fact that any decidable extension of MLS with the literals of type y = f [x] (map image operator) is ExpTime-hard (see next section) and the fact that the literal y = f [x] can be expressed in any extension of MLSS× 2,m with literals of type x0 = dom(f 0 ) by the literal y = dom((fx| )−1 ) . On the other hand, we observe that the language MLSS× 2,m allows one to express literals of the types dom(f ) ⊆ and f [x] ⊆ y, in view of the equivalences dom(f ) ⊆ x ⇐⇒ f = fx| f [x] ⊆ y ⇐⇒ f = fx|y . 4 ExpTime-hardness of MLS with the image operator In this section we provide a complexity lower bound for the satisfiability problem of the decidable extension MLSIm of MLS with literals of the type y = f [x].7 The semantics of the image operator f [x] is the obvious one, namely M (f [x]) = Def {v : [u, v] ∈ M f , for some u ∈ M x} , for any assignment M . Our result is achieved by reducing the decision problem for the description logic ALC to the satisfiability problem for MLSIm . ALC is a two-sorted language which contains: 7 MLSIm is a subfragment of a an extension of MLSS with some map constructs, whose decidability has been proved in [9]. 14 Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo – a countably infinite collection of concept names N c = {A, B, . . . }, – a countably infinite collection of role names N r = {P, Q, . . . }, – the symbols >, ⊥, representing the universal concept and the bottom concept, – the concept constructors ¬ (complement), u (conjunction), t (disjunction), ∀ (universal restriction), ∃ (existential restriction) to form complex concepts. ALC-concepts are defined recursively as follows: – concept names are concepts; – >, ⊥ are concepts; – if C, D are concepts, then ¬C, C u D, and C t D are concepts; – if C is a concept and R is a role name, then ∀R.C and ∃R.C are concepts. ALC-axioms have the following forms: – C v D (inclusion axiom), – C ≡ D (equivalence axiom), where C, D are ALC-concepts. The semantics of ALC is given in terms of interpretations.8 An interpretation I consists of a nonempty set ∆I , also called the domain of the interpretation, and of an interpretation function assigning to each concept name A ∈ N c a set AI ⊆ ∆I , and to every role name R ∈ N r , a binary relation RI ⊆ ∆I × ∆I . An interpretation I extends recursively to concepts as follows: >I = Def ∆I , ⊥I = Def ∅, (¬C)I = Def ∆I \ C I , (C t D)I = Def C I ∪ DI , (C u D)I = Def C I ∩ DI , (∀R.C)I I I I I  = Def u ∈ ∆I : (∀v ∈ ∆I )([u, v] ∈ RI −→ v ∈ C ) , (∃R.C)I = Def u ∈ ∆ : (∃v ∈ C )([u, v] ∈ R ) . Let I be an interpretation and let C, D be two concepts. Then I satisfies C v D (resp., C ≡ D) if C I ⊆ DI (resp., C I = DI ). In addition, let T be a finite collection of axioms. Then I satisfies T if and only if it satisfies each axiom in T ; also, I satisfies the concept C with respect to T if it satisfies T and C I 6= ∅. An ALC-concept C is said to be satisfiable with respect to a finite collection of axioms T if there exists an interpretation I that satisfies C with respect to T , otherwise it is unsatisfiable. If I satisfies a concept C (resp., a finite collection of axioms T ), then I is said to be a model for C (resp., T ). In [8, Theorem 3.27, page 132] the ExpTime-hardness of the problem of de- ciding if a given concept C is unsatisfiable with respect to a given finite collection T of inclusion axioms is proved for the sublogic AL of ALC. Hence, we have: 8 Here we recall just the descriptive semantic. There are several other semantics that are out of the scope of this paper. Title Suppressed Due to Excessive Length 15 Theorem 2. The problem of deciding whether a given ALC-concept C is un- satisfiable with respect to a given finite collection T of ALC-inclusion axioms is ExpTime-hard. t u Next we show how the satisfiability problem for ALC-concepts with respect to a finite set of axioms can be reduced to the satisfiability of MLSIm -formulae. Since ∃R.C ≡ ¬(∀R.(¬C)), without loss of generality we can consider only concepts that do not contain any occurrence of universal restriction. Theorem 3. The satisfiability problem for MLSIm is ExpTime-hard. Proof. In view of Theorem 2, it is enough to exhibit a reduction from ALC to MLSIm . Thus, given a finite collection T of ALC-inclusion axioms and an ALC- concept C, we show how to construct an MLSIm -formula which is satisfiable if and only if the concept C is satisfiable w.r.t. T . Let Cpts ⊆ N c and Rls ⊆ N r be the collections of the concept names and of the role names, respectively, occurring in C and in T . Additionally, let π be a function that injectively associates every concept name in Cpts to a set variable of the language MLSIm and every role name in Rls to a map variable of MLSIm . The function π extends naturally to concepts and axioms in the following recursive way: π(>) = Def U π(⊥) = Def ∅ π(¬C) = Def U \ π(C) π(C u D) = Def π(C) ∩ π(D) π(C t D) = Def π(C) ∪ π(D) π(∃R.C) = Def (π(R))[π(C)] π(C v D) = Def π(C) ⊆ π(D) π(C ≡ D) = Def π(C) = π(D) , where U is a set variable of MLSIm not in π[Cpts]. Let ϕ = Def ψ1 ∧ ψ2 ∧ ψ3 be the MLSIm -formula in which: V V ψ1 = Def U 6= ∅ ∧ A∈Cpts π(A) ⊆ U ∧ R∈Rls (π(R))[U] ⊆ U V ψ2 = Def Γ ∈T π(Γ ) ψ3 = Def π(C) 6= ∅. We observe that the size of the MLSS× 2,m -formula ϕ is linear in the total size of T and C. Next we show that ϕ is satisfiable (relative to the semantics of MLSIm ) if and only if C is satisfiable w.r.t. T (relative to the semantics of ALC). To begin with, let us assume that ϕ is satisfiable, and let M be a model for ϕ. We construct an interpretation I, induced by M , with domain ∆I = Def M U, by putting AI = Def M (π(A)) RI = Def ((M (π(R)))M U| )−1 , 16 Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo for every concept name A and role name R occurring in T or in C. Otherwise, the action of the interpretation I over the remaining concept and role names can be defined arbitrarily, as long as the constraints AI ⊆ ∆I and RI ⊆ ∆I × ∆I hold, for each concept name A and role name R not occurring in T or in C. Notice that since M models correctly all the literals in ψ1 , then we actually have AI ⊆ ∆I and RI ⊆ ∆I × ∆I for all concept names A and role names R, respectively, showing that I is a valid interpretation. Moreover, for every concept D involving only variables that occur in T and in C we have DI = M (π(D)) . (2) We prove (2) by structural induction on the concept D. If D is of type >, ⊥, ¬D0 , D0 t D00 , or D0 t D00 , then (2) follows directly from the definition of I. Thus, the only interesting case occurs when the concept D is of type (∃R.D0 ), with R a role name in Rls and D0 a concept structurally simpler than D. Let us show that (∃R.D0 )I = M (π(∃R.D0 )). Let v ∈ (∃R.D0 )I . Then there is a u ∈ D0I = M (π(D0 )) such that [v, u] ∈ R = ((M (π(R)))M U| )−1 . The latter implies [u, v] ∈ (M (π(R)))M U| , so that I [u, v] ∈ M (π(R)) (since u ∈ M U), and therefore v ∈ (M (π(R)))[M (π(D0 ))] = M (π(∃R.D0 )). Hence, (∃R.D0 )I ⊆ M (π(∃R.D0 )). To show the converse inclusion, let now v ∈ M (π(∃R.D0 )). Then v ∈ (M (πR))[M (π(D0 ))], so that [u, v] ∈ M (π(R)) for some u ∈ M (π(D0 )). There- fore [u, v] ∈ (M (π(R)))M (U)| (since by inductive hypothesis M (π(D0 )) = D0I ⊆ ∆I = M (U) and therefore u ∈ M (U)). Hence, [v, u] ∈ ((M (π(R)))M (U)| )−1 = RI . And since u ∈ D0I , then v ∈ (∃R.D0 )I . Therefore M (π(∃R.D0 )) ⊆ (∃R.D0 )I which together with the previous inclusion yields (∃R.D0 )I = M (π(∃R.D0 )). From (2) and the fact that M models correctly all the conjuncts of ψ2 , it follows that I is a model for T . Additionally, since M satisfies ψ3 , it also follows that I satisfies C, so that the interpretation I induced by the model M satisfies C w.r.t. T . This completes the first half of the proof. Conversely, let I be a model for C w.r.t. T . Without loss of generality, we may assume that ∆I is a set belonging to the von Neumann hierarchy V (otherwise, we embed ∆I in V). We construct an assignment MI induced by I as follows: MI (U) = Def ∆I ; MI (π(A)) = Def AI ; MI (π(R)) = Def (RI )−1 for all concept names A and role names R occurring in T and in C (as usual, we do not need to be specific on the remaining variables of MLSIm ), and show that MI is a model for ϕ. Much as was done before, we prove by structural induction that MI (π(D)) = DI , (3) for every concept D involving only concept and role names occurring in T and C. As before, the only relevant case to be considered is when D is of type Title Suppressed Due to Excessive Length 17 (∃R.D0 ). To prove (3) for a concept D of type (∃R.D0 ), it is enough to show that MI (π(R))[MI (π(D0 ))] = (∃R.D0 )I . Let u ∈ (∃R.D0 )I . Then there is a v ∈ D0I such that [u, v] ∈ RI . Therefore [v, u] ∈ MI (π(R)) and since by inductive hypothesis v ∈ MI (π(D0 )), it follows that u ∈ MI ((π(R))[π(D0 )]). Hence we have (∃R.D0 )I ⊆ MI (π(R))[MI (π(D0 ))]. To prove the converse inclusion, let u ∈ MI (π(R))[π(D0 )]). Hence, there ex- ists v ∈ MI (π(D0 )) such that [v, u] ∈ MI (π(R)) = (RI )−1 . But then [u, v] ∈ RI and since by inductive hypothesis MI (π(D0 )) = D0I , we have v ∈ D0I , and thus u ∈ (∃R.D0 )I . Therefore we have MI (π(R))[MI (π(D0 ))] ⊆ (∃R.D0 )I , which to- gether with the previously established inclusion yields MI (π(R))[MI (π(D0 ))] = (∃R.D0 )I . Having established (3), it is immediate to check that the assignment MI satisfies the MLSS×2,m -formula ϕ, completing the proof of the theorem. t u 5 Conclusions and Future Work We have introduced the unquantified fragment MLSS× 2,m of set theory, involving besides the basic set constructors, also the Cartesian product operator and some map constructs. We have shown that the satisfiability problem for MLSS× 2,m - formulae is NP-complete. We have also proved that any decidable extension of the basic fragment MLS extended with map literals of the form y = f [x] has an ExpTime-hard decision problem. Such lower bound has been obtained by exhibiting a reduction from the description logic ALC. We plan to further investigate the relationship between description logics and other MLS extensions in order to find new lower bounds. In particular, we conjecture that the presence of the map union and map difference operators together with the image operator leads to NExpTime-hardness. We also intend to extend the fragment MLSS× 2,m with some further map constructs such as reflexive closure, transitive closure, symmetric closure, and restricted forms of map composition. Furthermore, we plan to continue our investigations of decision procedure for a one-sorted variant of the language MLSS× 2,m in which maps (and the Cartesian product) are regarded just as primitive sets. References 1. D. Cantone and A. Ferro. Techniques of computable set theory with applications to proof verification. Comm. Pure Appl. Math., XLVIII(9-10):1–45, 1995. 2. D. Cantone, A. Ferro, and E. G. Omodeo. Computable set theory. Number 6 in International Series of Monographs on Computer Science, Oxford Science Publi- cations. Clarendon Press, Oxford, UK, 1989. 3. D. Cantone, A. Formisano, E. G. Omodeo, and J. T. Schwartz. Various commonly occurring decidable extensions of multi-level syllogistic. In S. Ranise and C. Tinelli, editors, Proceedings of the Workshop on Pragmatics of Decision Procedures in Au- tomated Reasoning 2003 - PDPAR’03 (Miami, USA, July 29, 2003), pages 2–14, 2003. 18 Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo 4. D. Cantone, E. G. Omodeo, and A. Policriti. The automation of syllogistic. II: Optimization and complexity issues. Journal of Automated Reasoning, 6(2):173– 187, June 1990. 5. D. Cantone, E. G. Omodeo, and A. Policriti. Set theory for computing - From decision procedures to declarative programming with sets. Monographs in Computer Science. Springer-Verlag, New York, 2001. 6. D. Cantone, E. G. Omodeo, J. T. Schwartz, and P. Ursino. Notes from the logbook of a proof-checker’s project. In N. Dershowitz, editor, Verification: Theory and Practice (Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday), volume 2772 of Lecture Notes in Computer Science, pages 182–207, Berlin, 2003. Springer-Verlag. 7. D. Cantone and J. T. Schwartz. Decision procedures for elementary sublanguages of set theory. XI: Multilevel syllogistic extended by some elementary map constructs. Journal of Automated Reasoning, 7(2):231–256, June 1991. 8. F. M. Donini. Complexity of reasoning. In F. Baader, D. Calvanese, D. L. McGuin- ness, D. Nardi, and P. F. Patel-Schneider, editors, The description logic handbook: theory, implementation, and applications, chapter 3, pages 105–145. Cambridge University Press, 2nd edition, 2007. 9. A. Ferro, E. G. Omodeo, and J. T. Schwartz. Decision procedures for some frag- ments of set theory. In W. Bibel and R. A. Kowalski, editors, In 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, volume 87 of Lecture Notes in Computer Science, pages 88–96. Springer, 1980. 10. E. G. Omodeo, D. Cantone, A. Policriti, and J. T. Schwartz. A Computerized Ref- eree. In M. Schaerf and O. Stock, editors, Reasoning, Action and Interaction in AI Theories and Systems – Essays dedicated to Luigia Carlucci Aiello, volume 4155 of Lecture Notes in Artificial Intelligence, pages 117–139. Springer Berlin/Heidelberg, 2006. 11. E. G. Omodeo and J. T. Schwartz. A ‘Theory’ mechanism for a proof-verifier based on first-order set theory. In A. Kakas and F. Sadri, editors, Computational Logic: Logic Programming and beyond, Essays in honour of Robert Kowalski, part II, volume 2408 of LNCS, pages 214–230. Springer-Verlag, 2002. 12. F. Parlamento, A. Policriti, and K. P. S. B. Rao. Witnessing differences without redundancies. Proc. Amer. Math. Soc., 125:587–594, 1997. 13. J. T. Schwartz. A survey of program proof technology. Technical Report 001, New York University, Department of Computer Science, September 1978. 14. J. T. Schwartz, R. B. Dewar, E. Schonberg, and E. Dubinsky. Programming with sets; an introduction to SETL. Springer-Verlag New York, Inc., New York, NY, USA, 1986.