Computer Science Department



TECHNICAL REPORT



The automation of syllogistic.
II. Optimization and complexity issues. *

D. Cantone

E.G. Omodeo

A. Policriti



Technical Report 405
October 1988



NEW YORK UNIVERSITY



in
o

I

K
Eh



CJQ
CO

s



o
u



a;
c
o
-p

D C
(0
U



CM



O



O M

M

c
o •

•H O

(0 4J

e w

O -H
4J -P

a o

rH

x: w

Eh




' Department of Computer Science
Courant Institute of Mathematical Sciences

251 MERCER STREET, NEW YORK, N.Y. 10012



The automation of syllogistic.
II. Optimization and complexity issues. *

D. Cantone

E.G. Omodeo

A. Policriti



Technical Report 405
October 1988



^Research supported by EM and ENIDATA within the AXL project.



The automation of syllogistic.
II. Optimization and complexity issues. *

D. CANTONE

Courant Institute of Mathematical Sciences, New York University

and University of Catania, Italy

E.G. OMODEO
ENIDATA-Bologna, Italy

A. POLICRITI
Courant Institute of Mathematical Sciences, New York University



Beyond that, and much more difficult still, is the problem of han-
dling the membership relation m an efficient way, so that theorem-
proving poblems involving set theoretic notions can be treated
(J. A. Robinson, 1967)

Abstract

In the first paper of this series it was shown that any unquantified
fonnala p in the collection MLSSF (multilevel syllogistic extended with
the singleton operator and the predicate Finite) can be decomposed as
a disjunction of set-theoretic formulae called syllogtstic schemes. The
syllogistic schemes are satisfiable and no two of them have a model in
common, therefore the previous result already implied the decidability
of the class MLSSF by simply checking if the set of syUogistic schemes
associated with the given formula is empty.

In the first section of this paper a new and improved searching algo-
rithm for syUogistic schemes is introduced, based on a proof of existence of
a 'minimum effort' scheme for any given satisfiable formula in MLSF. The
adgorithm addressed above can be piloted quite effectively even though it
involves backtracking.

In the second part of the paper complexity issues are studied by show-
ing that the class of ('i)o-stmple prenex formulae (an extension of MLS)
has a decision problem which is NP-complete. The decision cilgorithm
that proves the membership of this decision problem to NP can be seen
as a different decision algorithm for MLS.



"Fle»earch supported by ENI and ENID ATA within the AXL project.



1 Introduction

In the first paper of this series, [CG088], a family E of set-theoretic formu-
lae, cabled syllogiaiic schemes related to X, was introduced for any given finite
collection X of set- variables. It was proved that every syllogistic scheme is satis-
fiable, that is, it can be made true by suitably substituting sets for the variables
occurring in it. Moreover no two syllogistic schemes related to the same X in
E(X) have any model in common.

It was shown in the same article that any unquantified formula p in the
collection MLSSF (see below) cam be decomposed as a disjunction of syllogistic
schemes. A naive algorithm for determining whether or not a given p in F
is satisfiable is to calculate the set Ep of all disjuncts of p' and then check
whether this set is non-empty. A technique was established for extracting the
schemes that form Ep from the collection E( X ) of all syllogistic schemes over
the variables X of p. In other words, this is a technique for evaluating p in any
cr € E( A" ); in fact, is TRUE.

In the first pairt of this paper we improve the decision ailgorithm outlined
above, restricting our attention to formulae in MLSF. These formulae involve, in
addition to (9 and set-variables, the binary constructs D, \, U, S, C, =, the unary
relator Finite, and the propositional connectives. Therefore, the only construct
of MLSSF not taken into account in this paper is {•,...,•}. We will be able
to characterize the schemes directly, instead of being obtained by filtering out the schemes in E(X) that do
not satisfy p. We also prove that if Ep is non-empty, then it contains 'minimum
effort' schemes (in a sense to be explained in the next paragraph — and, in more
detail, in the next section). Thus in order to check p for satisfiability only such
schemes are to be sought for.

To be more specific, even at this informal level of discussion, we anticipate
that every syllogistic scheme where — is an equivalence relation over X and G is a directed acyclic graph
(or "DAG") whose nodes are the ~-classes. We will see that any (t in Ep
corresponds to an equivalence relation ~ of a particular kind, which will be
called a p-compatible relation, and a DAG of a particular kind, to be called a
p- — compatible DAG. If Ep is non-empty, then a finest p-compatible relation ~p
exists (this would no longer be the case if the construct {•,...,•} was admitted).
Moreover this relation, which can be determined by methods of propositional
calculus (see [Men64]), provably has some cr in Ep associated to it. Any a
zissociated to ~p is what we have called above a minimum effort syllogistic
scheme; estabUshing the existence of one such scheme amounts to searching for
a p-~p-compatible DAG. This search, although it involves backtracking, can be
piloted quite effectively (see [Omo84,G085]). In the second part of this paper
complexity issues on the decision problem for classes of set-theoretic formulas are
studied. In particular the class of (V)o-s;mp/e prenex formulae (an extension of



MLSS) is mtroduced and \a proved to be NP-complete. The decision algorithm
presented in the second part of the paper differs from the one presented in the
first part and provides another possible approach to the decision problem for
extensions of MLS.

Even this second edgorithm aissociates a graph to the formula to be decided.
The graph keeps information about a possible model of the formula in two
ways: by using the nodes and the edges of the graph to represent the sets in
the model, some of their elements auid the membership relation among them,
and by defining a map from the graph onto the hereditarily finite sets which is
obtained by induction and preserves all the properties of the model expressible
by (V)o-8iinple prenex formulae.

It turns out that, when the formula is satisfiable, that the algorithm can run
in polynomial time on a nondeterministic Turing machine.

Refined versions of this algorithm are presented in [PPm] to prove the decid-
ability of an extension of the class of (V)o-simple prenex formulae and to study
the decision problem of calsses of formulae involving a choice operator q.

2 A decision algorithm for MLSF

The constituents of the theory MLSF are:

• a denumerable infinity of set variables x, y,z, . . .;

• the operator U (binary union), D (binary intersection), \ (set difference);

• the predicates = (equality), 6 (membership). Finite (finiteness), C (set-
inclusion);

• the boolean connectives -•, A, V, — ►, «-►.

By a simple normalization process (see Section 3.8), the satisfiability problem
for MLSF can be reduced to the problem of testing for satisfiability conjunctions
of literals of the following types:

{ = ) X = y, X = y U z, X = y \ z,

{^)x^y,

{e, i) X € y, X i y,

{{•))T = {y},

( F , f ) Finite x, -â–  Finite x,

where each x , y , z is a set variable.

Let p be such a conjunction, and let X he the set of all variables appearing
in p. We denote by p= the conjunction of the literals of type ( = ) belonging to



p. Moreover, p, will stand for the propositional formula obtained from p- by
replacing the symbols =, U, and \ by ♦-►, V, and &-> respectively, and accord-
ingly regarding each set variable as a propositional variable. (Notice that in
our use of the word 'propositional' we are conforming here to a well-estabUshed
tradition — see, e.g., [Men64]. In particular, by 'propositional variable' we mean
a variable that ranges over the truth values FALSE, TRUE.)

In the following definition of a p-compaiible equivalence relation ~ over X,
our aim is to capture the properties that ~ must enjoy in order that it can be
"induced" by a model M of p, in the sense that i ~ y if and only if r = y is
true in M, for all I, y in X. It will be obvious that there exists an algorithm
for establishing whether any given ~ is p-compatible or not.

Definition 1 Let ~ be an equivalence relation over the set X of all variables
that occur in a given conjunction p of literals (=), {^), (€, ^) and {F, ^);
moreover, let p^ denote the propositional formula p, k, ^x~y {x «-► y).

An acceptable place of the pairp, ~ is any set P C X whose characteristic
function XP »^ " model ofp^, where

, . _ r TRUE ifx € P :
^Py"") - \ FALSE ifx e X \P.

By abuse of language, we will often say that a place satisfies a given propositional
formula to actually mean that its characteristic function satisfies it.

An equivalence relation ~ over X is said to be p-compatible iff the following
conditions are met:

(a) V '^ w if (and only if) v ^^ w is satisfied by every acceptable place of
P. ~;

(b) ifv^w belongs to p, then v 7^ w;

(cJifv£zo,w^ zi belong to p and zq ~ zi, then v 7^ w;

(d) if -< Finite V belongs to p then there must exist an acceptable place P„ such
that V € Pv and P„ does not contain any variable w for which Finite w
belongs to p.

The following lemma shows that any satisfiable conjunction p admits p-
compatible equivalence relations, induced by the models of p:

Lemma 1 Let M be a model of p, and let x ~m V if and only if x^ = y^ .
Then

(L) Pi = {x £ X : ^ € x^ } is an acceptable place of p, ~Mi where
(II) ~jvf is p-compatible.



Proof. Let ^ € Urgx ^^ ■ Clearly if i ~,\f y, then XP,(a?) = Xp, (y)< ie-
(i «-► y)''"'* = TRUE. Moreover if x «-► (y V z) is in p., then x = y u z is in
pand x^ = y^ U z" .

Hence ^ € x^ if and only if either ^ € y*^ or ^ 6 z''^, i.e. x/»«(2:) =
Xi»«(y) V x/»<(^). proving that xp, ia a model for x «-♦ y V z. Analogously it
can be shown that xp< satisfies all remaining conjuncts in p^, which proves that
XP^ is an acceptable place of p, ~Af, establishing (I). Note in addition that xp«
also satisfies all formulae -"(v ♦-► w) for which ^ € {v^ \ w'^) U [w^ \ v^).

Next we show that ~Af is p-compatible. First of all. it is clear that ~Af is
an equivalence relation. If t; '/'m w, for any two variables v, w occurring in p,
then v^ ^ w^, so that there exists ^ € {v'^ \ w'^) U {w^ \ v"). Therefore
(y «- «;)'"'« = FALSE, est (a) of Definition 1.

(b) is an immediate consequence of the very definition of ~Af . in view of the
fact that M satisfies p.

If V 6 zo> w ^ zi belong to p and zq ~Af 2\, then v''' € Zg*, w^ ^ zf ,
and Zq* = zf , which imply v^ ^ u;^ and in turn v -^m w- Having thus
shown that (c) of Definition I holds too, we now proceed to prove the only
remaining condition, (d). Let us assume that -• Finite v belongs to p. Hence v^^
is infinite. By (I), P( is an acceptable place of p, ~Af for every ^ in v'^; moreover,
since obviously there are only finitely many acceptable places of p, â– ^\f, it follows
that there must exist an acceptable place P such that { ^ € v^ : P^ = P}
is infinite. So, if u; € P, then {^ e v^ : P( = P] C ti;^, i.e. ti;'^is
infinite, auid hence Finite w cannot belong to p. This completes the proof of
the p-compatibility of ~Af > establishing the lemma. â– 

An important equivalence relation is introduced by the following definition.
Definition 2 Given p as above, for any x and y occurring in p we put

X ^p y ff and only :/ p, — ♦ (i •-► y) is tautological,
where p, is obtained from p as in Definition 1.
Lemma 2 ^p is an equivalence relation.

Proof. The lemma follows at once from the reflexivity, symmetry and trauisi-
tivity of «-••■. ■

An important property of the equivalence relation ~p is stated in the fol-
lowing lemma.

Lemma 3 Let ~ be a p-compatible equivalence relation. Then

(i) t/x ~p y then i ~ y, for x, y in X;
(ii) ~p IS p-compattble.



(In other words, ~p is the finest p-compatible equivalence relation over the set
X of variables occurring in p).

Proof. Let x ~p y. Then p« — ► (x ♦-► y) is a tautology. If P is an acceptable
place of p, ~, then XP satisfies p^, eind in particular p.. Hence (i *-♦ y)^'' =
TRUE. This shows that x <-♦ y is satisfied by all acceptable places of p, ~.
Therefore the p-compatibility of— implies x — y, establishing (i).

In order to prove that ~p is p-compatible, we show that conditions (a)-(d)
of Definition 1 are met for ~p. Observe that the acceptable places of p, ~p are
those sets P such that xp satisfies p.. Therefore, if u «-► lo is satisfied by every
acceptable place of p, —p, it follows that p. — ♦ (v «-* u;) is a tautology, i.e.
V ~p w, proving (a).

To establish (b), assume that v ^ w occurs in p. If i; ~p w, then by (i)
above v ^ w, contradicting the p-compatibility of ~. Thus v y-p w, and (b) is
proved.

Next suppose that zq ~p zi, and assume also that r € zo and lu ^ zi occur
in p. Then again by (i) zo ~ ^ii implying v -/' w Thus, as above, v -/-p w,
concluding the verification of (c).

Finally, let -> Finite v occur in p. From the p-compatibility of ~ it follows
that there exists an acceptable place P„ of p, ~ such that v € Pv not containing
any variable w for which Finite w occurs in p. Then it is enough to observe
that P„ is also an acceptable place of p, ~p. This shows that (d) of Definition 1
is also fulfilled, which in turn establishes (ii) of the present lemma. â– 

An immediate consequence of the preceding lemma is given in the following
corollary.

Corollary 1 If p is satisfiable, then ~p is p-compatible.

Proof. Let M be a model of p. Lemma 1 shows that ~a/ is p-compatible, and
therefore Lemma 3 entails the p-compatibiUty of —p. ■

The preceding corollary says that the p-compatibility of ~p is a necessary
(algorithmic ally verifiable) condition for p to be satisfiable. In what follows, we
will bring to light another necessary condition for the satisfiability of p. Taken
together with the p-compatibility of ~p, the latter condition will suffice to imply
that p admits a model Mp such that ~p coincides with ~Af, (cf. Lemma 1).

In view of LemmM 1(11), 3(i), this will entail that when p is satisfiable then
any two variables x, y of p are ~Mp -equivalent if and only if x ~jvf y (i.e., the
set-values of i and y coincide) in every model M of p.

We incidentally note that the existence of a finest equivalence ~Af , with M
a model of p, is no longer insured if one adds new operators to those admitted
in MLSF. For example, the models of the formula

z = z\z&s=: {x} &c y \ s = z



of MLSSF can be grouped into two classes, with

y ~Afo ^ - y i'Mo « .

y ~M, ^> y T^.vf, s

(and hence

y ~.Wo ' °ot implying y ~,v, z,

y ~Af, i not implying y ~.v„ z )

whenever Mo belongs to the first class and M\ belongs to the second. Other
formulas with similar pathology are y ^ {a, h\ k. a ^ h and x, y, z ^ {Oi^}-

The above discussion indicates that ~p is mainly related to the equalities
holding in a sought model of p. To fully take into account the membership
literals as well, we introduce the p — -compa
Definition 3 Let ~ be a p-compatible equivalence relation and let S be the col-
lection of representatives of the variables occurring m p (for example, «/ we
assume that all variables of set theory are arranged in a denumerable sequence,
then we can choose the first variable m each equivalence class C as the repre-
sentative of C). A DAG (S, ') is said to be p-~-compatible tff

(a) u = Po n S, for each v in S, where P^ is an acceptable place of p, ~;

(b) ifv 6 w [respectively: v ^ wj occurs in p, then s^ € s'v, [resp.: 3^ ^ s'v]

where ««,««, € S and s„ ~ u, a„^ ~ u;.

Later in this section we will show that a normEdized conjunction p of MLSF
has a model if and only if ~p is p-compatible and there exists a p — ^p-compatible
DAG {Sp , '), where Sp is the set of all ~p-representatives. This provides at
once a satisfiability algorithm (alternative to the one described in Corollary 1)
for MLSF: in fact, the number of possible DAGs {Sp , ') is clearly finite and,
moreover, there is an algorithm to test whether a given DAG is p-~p-compatible.

A first step towards proving the completeness of the above test is the fol-
lowing lenruna.

Lemma 4 If p is satisfiable, then there exists a p-compatible equivalence rela-
tion ~ which admits a p — -compatible DAG.

Proof. Let M be a model of p. Consider the relation ~,\f defined by putting
X ~.v/ y if and only if x'^ = y^. (II) of Lemma 1 shows that ~v is p-
compatible. It only remains to show that the set 5.v/ of ~.\/-representative3 of
the variables of p can be given the structure of a p-~.vf -compatible DAG. To
this end we put

i} = {w £ Sm : v' € xv^ }, for every v in S\{ ,

so that ii = { X e X : u'^ G r"^ } n Sjvf , where ,Y denotes the collection of all
variables occurring in p. Since by Lemma 1(1) the set { i € -Y : v'"^ G x'^^ }



ia an acceptable place of p, ~Af, (a) of Definition 4 is satisfied. Observing that
(b) of the same definition is aui immediate consequence of the fact that M is a
model of p, it follows that {Sm , * ) is a p — Af-compatible DAG, which proves
the lemma. â– 

Lemma 5 Let p be a normalized conjunction of MLSF. If there exists a p-
compatible equivalence relation ~ admitting a p-~-compatible DAG, then ~p
(cf. Definition 2) is also p-compatible and admits a p-'^ M-<^ompatible DAG.

Proof. Lemma 7 ensures the p-compatibUity of ~p. Next, let {S^ , " ) be a
p-~-compatible DAG. We will show how the set Sp of ~p-representatives of the
variables occurring in p can be given a structure of p-~p-compatible DAG.

For each u in Sp let v» € S^ be such that t; ~ u;. and put v= { lo 6 Sp :
w» 6 V* }• We must simply show that {Sp , • ) is a p-~p-compatible DAG. Since
(S-, , ' ) is a DAG, so is (Sp , • ) • The p-'-p-compatibility of {Sp , • ) caui be
proved eis follows. Let v E Sp. As {S^ . * ) is p-~-compatible, v, = P r\ S^,

for some acceptable place P of p, ~. We have v = P r\ Sp. Indeed, ii w £.v
then tu, € v, = P C\ S^. In particular w, £ P, and since ti; ~ lu. we have
u; e P.

Therefore ly 6 P n Sp. Conversely, if ty € P C\ Sp, from the fact that P

is an cicceptable place of p, ~ it follows u;, 6 P H S.^ = v,, so that w Ev.
Hence (a) of Definition 3 is proved for {Sp , • ). .

Assume now that S-, 9 s„ ~ u ~p ^u G Sp and that S^ 9 Su, ~
i" ~p 5«; € Sp. Lenmia 3(i) impUes that g^ ~ s„ and g^ ~ s^, so that
gv= {x £ Sp : X, € s„ }. If u G lu occurs in p, then by the p-~-compatibility
of (S«. , * ) we have s^ 6 s'v showing g^, €gv If instead u ^ u; is a literal of
p, then flTu, ^gvi because otherwise {gw)» € s'«, i.e. s^ € s'^, which contradicts
the hypothesis of p-~-corapatibility of {S^ , ' ). This completes the proof that
{Sp , * ) is p-~p-compatible, and the lemma is established. â– 

From the preceding two lemmaa the following corollary is immediately de-
rived.

Corollary 2 (Completeness) Let p be a normalized conjunction of MLSF.
Ifp is saiisfiable then ~p is p-compatible and it admits a p-^p-compatible DAG.
Moreover, there is an algorithm to test whether '^p is p-compatible and it admits
a p-"^ p-compatible DAG.

In order to show the soundness of the test given in preceding corollary we
recall the definition and some properties of syllogistic schemes (cf. [CG088]).

DeRnition 4 Let X = {xq , Xi , . . . , x/ } and Y = { yo , yi , • • • , yy } be
collection of set variables such that

(i) X and Y have no variables in common;



(ii) there ts a bijection o : r — Pow(X) \ {0} (so that \Y\ = 2l^l - 1/

Moreover, lei ~ be an equivalence relation over X whose equivalence classes
are

{ rOO . lOl . • • • . ^OLo } ' { 2^10 . In . ■ • ■ > IlLi }.-••. { XNO . lATl > ■ • • . XNLs ) '

u)tM x„o -< ini -<•••-< inL. for n = 0, 1,..., ^, and uiAere we assume
loo -< iio -<••■-< xato r"< »* <* fixed ordering of the collection of all variables).
Let us put Sn = x„o for n = 0, 1, . . . , iV, and let S = {so , 8\ , . . . , arf} be
the set of representatives of the equivalence classes of~. Also suppose that S is
given a DAG structure {S , ' ) Let F C Z C Y be such thai

a) z C S, for all z m Z;

b) there are no distinct v, vu in S such that

bl) u € s if and only if w G «, for all s in S, and



b2) v € z if and only if w ^z, for all z in Z
hold together.

Lei 6 , gzF denote the formulae

^ =Def ^}
QZF =-Qei ^n
z^ z res

Sn €Z «n € r

(&/€F Finiteif) ) k ( &:,6z\f -■ Finite{z) ) .

We put (TzF — Def ^ ^ ^^^ "'"' '"''" ''^^'' " syllogistic scheme over X ('relative
to X , ~ , ').

In [CG088] it is shown that syllogistic schemes partition the class of all
possible assignements over X . Other important properties of syllogistic schemes
are stated in the following proposition (for a proof see [CG088]).

Proposition 1 Let (Tzf *« i syllogistic scheme relative to X , ■^ , ' . The fol-
lowing properties hold:

(a) ' solvable;

(b) for any solution M of
(bl) for all X, y in X, x^ = y'^ 'ffx^y,

(b2) for all sq.Si m X, s^ € s'^ iff sq- € si,

(b3) for all s in 5, s'^ is infinite iff s £z for some z ts Z \ F.



9



The following lemma gives the soundness of the satisfiability test whose
completeness has already been established in Corollary 2.

Lemma 6 (Soundness) Let p be a normalized conjunction of MLSF and let
X be the collection of all variables occurring in p. If there exists a p-compatible
equivalence relation ~ which admits a p-^-compatible DAG (S, ' ), then p is
satisfiable.

Proof. We will show that from the hypothesis it follows that there exists a
syllogistic scheme This, in view of Proposition 1, gives the result. We construct such a syllogistic
scheme as follows.

For each pair sqi s\ of distinct variables in S for which { x : so € i} =
{x : Si G i}, we consider an acceptable place P,o,i of p, ~ such that

So e P,o., iff«i i P»o*i-

Moreover, for each s in S for which -^Finite v occurs in p with s ~ u, we
consider an acceptable place P, such that s G P» and P, does not contain any
variable w with Finite u; occurring in p. Note that the existence of such places
Psosi and P, is insured by the p-compatibility of ~ (cf. Definition 1). Let Y
be a set of vairiables, disjoint from X, and let "• be a bijection from Y onto
Pow(X) \ { }. We denote by Z the set of all y in y with y = P n S, where
P is a place of the type P,o«i °' °f '^^ *yP® ^'- Moreover we denote by F the



set of all z in Z with z = P n S where P is not of the form P, . It is aji easy
matter to verify that (Tzf is a syllogistic scheme over X , ~, ' .

In order to complete the proof of the lemma it only remains to show that
every model of Lemmas 1, 2 imply at once that M correctly models all literals in p of type
ar = 2/, I ^ y, X 6 y, X ^ y. Finite x, and -< Finite x. U v = wi U W2
occurs in p, then supposing r ~ s„, ti;i ~ s„,j, and W2 ~ s^,,, we have (cf.
Definition 1)

v^ = s^ = U ^^U U {'•^}
z £ Z res







s„ ez s„ er

= ( U ^""^ U {'•''}) ^ ( U ^""^ U i^''})

zez res zez res

5^^ ez ^'"i ^ ^ s^, e'z ««-:. ^ ^

since, by the p-~-compatibiUty of (5 , * ), sets i and z are of the form P n S
for some acceptable place P of p, ~, so that s„ € P if and only if s^^ € P or



10



Sw, € P- This shows that M is a model of the literals in p of type v = wiUw^.
Analogously it cam be shown that the remaining clauses of type v = lyj \ 1^2
are also modeled correctly, thus showing that M is model of p. This completes
the proof of the lemma. â– 

Combining together Corollary 2 and Lemma 6 we re-discover that the class
MLSF of formulae has a decidable satisfiability problem:

Corollary 3 An algorithm for testing a normalized conjunction p of MLSF for
satisfiability is:

(1) construct the equivalence relation ~p;

(2) check whether ~p is p-compatible;

(3) check whether â– ^p admits a p-^ p-compatible DAG.

3 On Complexity Issues

3.1 The NP-completeness of (V)o-simple prenex formu-

1 2