Reasoning about distances

1 Introduction

The numerical notion of distance or metric as a measure of closeness or similarity (in a great variety of senses) plays a fundamental role in many branches of science-including, naturally, knowledge representation, artificial intelligence and informatics in general. Recent examples are such dif­ ferent fields as spatial KR&R and geographic information systems [Cohn and Hazarika, 2001; Adam and Gangopad­ hyay, 1997], computational molecular biology [Setubal and Meidanis, 1997; Clote and Backofen, 2000], text processing [Salton, 1989] and data mining [Dunham, 2003]. Unlike clas­ sical physics and the corresponding mathematical models, the 'distance spaces' arising in these applications may be quite different from the standard Euclidean spaces, e.g., they are often finite and do not necessarily satisfy all of the metric axioms. Another important feature is that properties of only some objects in the space may be known, and the task is to use the available information to determine properties of other elements of interest. Traditional methods of dealing with met­ ric data are mostly numerical or 'sub-symbolic' (e.g., graph­ theoretic or probabilistic) and usually do not involve any kind of (automated) reasoning which is based upon symbolic, ex­ plicit knowledge representation. The main aim of this paper is to present a new expressive logic-based formalism intended for reasoning about distances and to provide it with a tableau decision algorithm.

The language we propose is-as far as its algorithmic prop­ erties and expressiveness are concerned-a compromise be­ tween full first-order and propositional languages: it contains object names and unary atomic predicates from which com­ plex predicates are constructed by means of the Boolean operators and restricted quantifiers like, e.g., v<r ('for all objects within a circle of radius r') and :J<r ('for some object within a circle of radius r'). Thus, :J<rp denotes the set of all ob­ jects each of which is located at distance < r from at least one object with property P. To illustrate the expressive power of the language and to convince the reader that it can be useful, we give three concrete examples.

Example 1. Consider a space of proteins (i.e., sequences of amino acids); some of them are well studied, but properties of the majority are not known. Using one of the available techniques, we can define a 'similarity measure' between pro­ teins which gives rise to a certain 'distance' (perhaps, metric) space. One of the typical problems is to recognise whether a given protein p has some property P, e.g., whether it con­ tains an EF-hand motif. The usual approach of comparing the structure of p with that of 'closely located' proteins whose properties are known can be supplemented with a knowledge base composed by an expert and containing information like

• 3~ 5 Q n p = ..l - 'no protein located at distance :S 5 from a protein with a property Q has P ,'
• 3~ 2 { f} ~ R - 'all proteins located at distance :S 2 from a particular protein f have a property R,' etc.

Note that, in view of incomplete information about proper­ ties of elements of the distance space, to answer the query whether p can have P, we have to run a satisfiability-checking algorithm rather than a model-checking one.

Example 2. Suppose now that we are trying to organise a web site for selling books (or any other goods) on-line. One way of classifying the existing books is to introduce a mea­ sure of closeness of the contents of some of them. We then obtain a database containing items of the form o ( b1 , b2 ) = a, if the distance between books b1 and b2 is a, and, say, o ( b1 , b2) > c, for some number c, if the distance between b1 and b2 is only known to be greater than c. Now we can built a sort of terminology by saying:

• Harry _Potter E Fiction,
• Fiction n 3~ 3 Science ~ Science_Fiction,
• Science_Fiction ~ V~L,Science,
• :J< 1 AI n 3~ 1 Science_Fiction :f. ..l,
• V9Computer _Science ~ Science, etc.,

and deduce, for instance, that AI is not subsumed by Com­ puter Science.

Example 3. Perhaps the most natural application of this kind of formalism is spatial representation and reasoning. We can speak in terms of 'absolute' distances:

• 8(London, Leipzig) > 100,
• house E:J< 1 \f::0: 0 · 5 (shop u restaurant) - 'the house is located within 1 mile distance from a shopping centre of radius 0.5,'
• doughnut = 3::0: 10 {centre} n -,:J< 6 {centre}.

We can also deal with distances given implicitly by saying, for example,

• 8(London, Leipzig) > 3 · 8(Liverpool, Manchester),
• my_house E:J<xcollege, 8(Dov' s_house, college) ='= x ('I do not want to have a house that is located farther from my college than Dov's house')

without referring to concrete distances between the cities and perhaps having no idea where Dov's house is.

The approach to reasoning about distances we advocate in this paper has grown up from four main sources. First, extensive research has been done by the (spatial/constraint) database community [Revesz, 2002] aiming to deal efficiently with large sets of data which come equipped with some kind of distance (or similarity) measure; consult, e.g., the litera­ ture on 'similarity search' and 'k-nearest neighbour queries' [Bozkaya and Ozsoyoglu, 1999; Hjaltason and Samet, 1999]. Although this paper does not contribute to this field, 1 we were driven by the idea that it may be useful to extend the 'evaluation-based' methods by automated reasoning services. As was mentioned above, complete information about models based on distance spaces, and even distances themselves, are often not available, which means that the quality of solutions provided by the database technology can be significantly im­ proved by using explicit knowledge of the field (or even con­ jectures) supported by appropriate reasoning procedures.

Two approaches to extend the database technology by means of KR&R have been developed by the qualitative spa­ tial reasoning community. One is based upon the representa­ tion of spatial data by means of constraint systems [Renz and Nebel, 1999], while the other uses first-order theories, e.g., [Randell et al., 1992]. Constraint systems are usually very efficient (at most NP-complete); however, their expressive power is rather limited (for instance, they do not allow any kind of quantification). On the other hand, the unrestricted quantification of first-order representations is a serious obsta­ cle for their use in practical reasoning systems.

In a sense, our approach is similar to that taken by the description logic community which represents conceptual knowledge by means of restricted quantification (a kind of modal necessity and possibility operators) and uses reason­ ably effective tableau-based procedures even for expressive and complex (say, EXPTIME-complete) formalisms [Hor­ rocks, 1998]. The chief difference from description logics is that we have to integrate rather sophisticated reasoning about quantitative data into a logic-based framework.

1 Note, however, that our logics can express some of the cluster­ ing conditions.

Logics of distance spaces were introduced in [Sturm et al., 2000; Kutz et al., 2003], where our main concern was to find out whether such logics can be decidable. Unfortu­ nately, the logics constructed in these papers were not sup­ ported by effective reasoning machinery. The aim of this paper is more practical. To begin with, in Section 2, we present an application oriented variant MS~ [<Q+] of a dis­ tance logic (containing location constants, set variables and restricted quantifiers) and show that the satisfiability problem for its formulas in metric (and some weaker distance) spaces is EXPTIME-complete. As distance spaces used in computer science and AI are often finite (e.g., data with a similarity measure, a model of a railway system, etc.), we consider also the problem of satisfiability of MS~ [Q+] knowledge bases in finite spaces. We show that the language does not 'feel' the difference between finite and infinite spaces: all the results presented for satisfiability in arbitrary spaces hold for finite spaces as well. (Unfortunately, if we restrict attention to the two-dimensional Euclidean space or its subspaces, then the satisfiability problem becomes undecidable.) Then, in Sec­ tion 3, we devise a tableau-based satisfiability checking al­ gorithm for this logic. An interesting and quite unexpected consequence of the proofs of these results is the following observation. The full MS~ [Q+] contains both operators :J :Sa and :J<a which together allow assertions like

• houseE39shopn-,:J< 1 shop- 'the closest shop is located in precisely 1 mile distance from the house.'

But in everyday life we often do not pay attention to the boundaries of spatial regions or treat them in a sort of vague manner. What happens if we keep only one of the operators 3:Sa or :J<a in our language? Do the two resulting fragments behave differently, or to put it another way, does our language feel the difference between regions with and without bound­ aries? To our surprise, the answer turns out to be 'NO' (for a precise formulation of the result see Theorem 7).

To be able to express knowledge about implicit or unknown distances, in Section 4 we extend MS~ [Q+] with variables ranging over distances and prove that tFie satisfiability prob­ lem for the resulting language is decidable.

Because of lack of space we had to omit all (rather non­ trivial and lengthy) proofs. They are available at http: I I www. esc .liv. ac. uk/~frank). Here we only say that the complexity result as well as the proof of the correctness and completeness of the tableau algorithm are based on a rep­ resentation of metric spaces in the form of relational struc­ tures a La Kripke frames. This representation allows us to use advanced techniques from modal and description logics.

2 The logic MS~ [ M]

Let M be a non-empty subset of positive rational numbers (i.e., a subset of Q+). Denote by MS~ [M] the language with the following alphabet and term anoformula formation rules. The alphabet consists of

• an infinite list of set (or region) variables X 1, X2, ... ;
• an infinite list of location constants £1, fz ... ,

• the set constant (or nominal) { fi}, for every£;,
• binary distance (8), equality(:::::::) and membership (E) predicates;
• the Boolean operators n, --, (and their derivatives U, T and ..l) ;
• two distance quantifiers :::J<a' :::J :S:a and their duals v<a' \:f :S:a , for every a EM;
• two universal quantifiers :::3 and\:/.

Set terms 8 of MS~[M] are defined as

and the formulas of MS~[M] are

• f E8, where £ is a location constant and 8 a set term,
• 8 ::::::: t and 8 #:- t, where 8 and t are set terms,
• and all 'distance atoms' of the form 8(k,£) <a, 8(k,£) :Sa, 8(k,£) >a, 8(k,£) 2: a, where k, £ are location constants and a E M .

We use 81 !::;; 82 as an abbreviation for 81 n 82 = 81.

The intended semantics for this language is defined as fol­ lows. An MS~ [M]-model is a structure of the form

where (W, d) is a metric space with a distance function d satisfying the axioms

forallx,y,z E W,X;'l 3 ~ W,and£~ E W. Thus,IEdefines explicitly the values of set variables and location constants. (Although we do not make the unique name assumption­ i.e., e~ = er' i f:. j, is not prohibited-it is easy to force different location constants to denote different points by in­ cluding{£;}!::;; ·{fj} into the knowledge base.) The values 8 'B of other MS~ [ M]-terms 8 in IE are computed inductively as follows: -

The truth-relation IE F cp, where cp is an MS~ [M]-formula, is defined in the natural way: -

• IE F £E8 iff f'B E 8'B,
• IE F 81 = 82 iff 8~ = 8~ (and IE F 81 #:- 82 iff 8~ f:. 8~),
• IE F 8(k ,£) :Sa iff d(k'B,f'B) :Sa,
• IE F 8(k,£) <a iff d(k'B,f'B) < a,andsimilarfor2: and>.

An MS~[M]-knowledge base is a finite set of MS~[M]­ formulas:-A knowledge base I: is called consistent (or satisfi­ able) if there exists an MS~ [M]-modeliE such that IE F cp for all cp E I:; in this case we write IE F I:.

The language MS~ [ M] is a proper fragment of the lan­ guage MS[M] introduced in [Kutz et al., 2003]. While MS[M] has the interesting property of being of the same expressive power as the two-variable fragment of first-order logic over metric spaces, reasoning in MS[M] is undecid­ able. [Kutz et al., 2003] investigates in-depth the fragment MS"[M] of MS[M] with distance operators :::J :S:a , :::J >a ('for some object outside a circle of radius a') and their duals. In particular, various decidability results are obtained. The ex­ pressivity of MS~[M] and MS"[M] is incomparable and the mathematics re-quired to analyse these logics differs con­ siderably. The tableau-algorithm presented here shows that MS~ [ M] is probably more suitable for efficient reasoning than MS"[M].

Our first result establishes the decidability and the computational complexity of the satisfiability problem for MS~ [M]-knowledge bases in metric spaces:

Theorem 4. The satisfiability problem for MS~[M]­ knowledge bases in arbitrary metric spaces is EXPT!ME­ complete (even if the parameters from M are coded in bi­ nary).

Actually the same result can be proved for satisfiability in weaker distance spaces, say, the class of spaces which do not necessarily satisfy the triangular inequality (2) or the symme­ try axiom (3). The proof of this and some other theorems in this paper are based on a rather sophisticated representation of distance spaces in the form of relational structures a la Kripke frames. The EXPTIME satisfiability-checking algo­ rithm is basically an elimination procedure which iteratively deletes from the set of all 1-types over a sufficiently small set of terms all those that contain distance quantifiers without witnesses.

According to the next result, the logic of metric spaces in­ troduced above has the finite model property, and so Theo­ rem 4 holds for the class of finite metric spaces as well (the third equivalence actually follows immediately from the fact that any finite metric space is isometric to a subspace of some L~, n E N+ [Matousek, 2002]).

Theorem 5. The following conditions are equivalent for any MS~ [M]-knowledge base I: :

• I; is satisfiable in a metric space;
• I: is satisfiable in a finite metric space;
• I; is satisfiable in a finite subspace of some space L~ =

It turns out, however, that these positive results do not hold if the intended metric space is the two-dimensional Euclidean space or the class of its subspaces (this result is proved by a reduction of the undecidable N x N-tiling problem):

Theorem 6. (i) Satisfiability of MS~[{1, 2}]-knowledge bases in subspaces oflR x lR is undecidaole.

(ii) The satisfiability problem forMS~ [ { 1, 2} ]-knowledge bases in lR x lR is undecidable. -

Denote by MS<[Q+] (MS"[Q+]) the fragment of MS~[Q+] without the quantifiers ::~:<::a and v::::a (:J<a and v<a, respectively).

Theorem 7. Suppose that ~ is a knowledge base over MS::;[Q+] and~' results from ~ by replacing all occur­ rences of'i::;a with v<a and 3:<::a with :J<a. Then ~ is sat­ isfiable iff~' is satisfiable.

3 The tableau algorithm

Our tableau algorithm is closely related to tableau-based de­ cision procedures from the field of description logic [Baader and Sattler, 2000]. However, in addition to the standard methodology of description logic, we have to take care of the 'arithmetical meaning' of the quantifiers.

Suppose that a knowledge base ~ is given. To simplify pre­ sentation, we will assume that~ is formulated in the language MS~ [N+] without universal quantifiers V and 3. (Knowl­ edge oases containing rational numbers can be transformed into knowledge bases over N without effecting their satisfia­ bility.)

Denote by trm(~) the set of set terms occurring in ~. Without loss of generality we may assume that ~ contains at least one parameter from r::~+ and one nominal { f;}. A set term 8 is in negation normal form (NNF) if -, occurs in 8 only in front of set variables and set constants. Each set term can clearly be transformed into an equivalent one in NNF by pushing-, inwards (e.g., -,:J<a 8 is equivalent to v<a,8). So we may assume all set terms to be in NNF. Distance atoms of MS~ [N+] can be expressed via nominals and distance quan­ tifierS, e.g.,

So, from now on we will not be considering distance atoms at all. Moreover, without loss of generality we may assume that the language MS~ [N+] contains no formulas of the form

f E 8. Indeed, every such formula is equivalent to { f} U 8 ::::: 8. We can also assume that all equalities 8 1 = 8 2 and their nega­ tions 8 1 :f. 82 are of the form 8 = T and 8 :f. l_, respectively. And by taking for each formula of the form 8 :f. j_ in ~ a fresh location constant f 8 and replacing 8 :f. j_ with fs E8, we can get rid of all negations of equalities.

To sum up: in what follows (without loss of generality) we confine ourselves to considering those knowledge bases

~ over N+ that contain only equalities of the form 8 = T , with 8 being in NNF.

Let Zoe(~) be the set of all location constants occurring in ~. Define the closure cl(~) of~ to be the finite set of terms containing trm(~) and, for all a E N+,

Denote by IE the maximal parameter which occurs in ~ and set

where the a- are not inN.

The tableau algorithm we are about to describe operates on constraint systems S = (T, <, L, S) for~. where (T, <) is a forest consisting of the disjoint union of finite intransi­ tive trees (Te, <e) with roots f E Zoe(~), and L and S are labelling functions such that

• with each pair x < y, x, y E T, the function L associates a number L( {x, y}) from M[~] U M[~]-;
• with each x E T the function S associates a subset S(x) ~ cl(~).

Roughly, the intuition behind this definition is as follows : T is the set of points of a metric space, L defines distances be­ tween some points in this space, and S defines values of set terms from cl(~).

We start with the initial constraint system (To, <o, L0 , 50 ) for~. where To= Zoe(~), <o= Lo = 0, and So(f) = { { f} } , for every f E Zoe(~). Then the initial constraint system is ex­ panded by repeatedly applying (in any order) the completion rules in Fig. 1, where blocked nodes are defined as follows.

Denote by <+ the transitive closure of <. We say that a node x E T is directly blocked by a node y if y <+ x, S(x) = S(y), but for no distinct u <+ x and v <+ x do we have S(u) = S(v). The<+ -successors of directly blocked nodes are called indirectly blocked. All directly or indirectly blocked nodes comprise the set of blocked nodes.

Constraint systems obtained by applying the completion rules to the initial constraint system for ~ will be called con­ straint systems for~. Such a constraint systemS is said to be complete if one of the following conditions hold:

1. S contains a node x such that X;, ·X; E S ( x), for some set variable X;;
2. S contains a node x, such that { f;}, -, { f;} E S ( x) for some location constant { f;};
3. none of the rules in Fig. 1 is applicable to S (in the sense that no application of a rule can change the constraint system).

In cases 1 and 2 we say that the constraint system contains a clash.

Theorem 8. The tableau algorithm, having started from any given constraint system ~. always terminates (i.e., reaches a complete constraint system after finitely manyl steps); it is sound (i.e., if there is a complete clash-free constraint system for~ then ~ is consistent) and complete (i.e., if~ is satisfi­ able, then the tableau algorithm returns a clash-free complete system).

2 lcl(E)I Actually, at most loc(:E) · I trm(EW +l.

• Rn If s1 n s2 E S(x) and xis not indirectly blocked, then set S(x) := S(x) U {s1, sz}.
• Ru If s1 U s2 E S(x) and xis not indirectly blocked, then set either S(x) := S(x) U {sd or S(x) := S(x) U {sz}.

• R3< If:J<as E S(x), xis not blocked, and for any z with s E S(z), then create a new node y > x and set L({x,y}) :=a- andS(y) := {s}.
• R3 :-:; If 3:Sas E S(x), xis not blocked, and L({z,x}) ~ {b: b:::; a} U {b-: b:::; a} for any z with s E S(z), then create a new node y > x and set L({x,y}) := aandS(y) := {s}.

Figure I: Tableau rules.

It is to be noted that the rule Rv is rather inefficient as it stands. Actually, there is no need to add those V9 sand v<b s, but then some other rules, as well as the blocking strategy, have to be changed in a subtle way. We show here this 'ineffi­ cient variant' to make the tableaux as transparent as possible. The worst case complexity (even of the more efficient vari­ ant) of the tableau algorithm does not match the EXPTIME upper bound of Theorem 4, which is actually a feature of all implemented tableau procedures in description logic.

4 Metric logic with numerical variables

Let us consider now the language MS~ [V] which is defined almost precisely as MS~[M], with th-; only difference being that instead of parameters (numbers) from M we use variables from a countably infinite list V = { x0 , x1 . .. } ranging over Q+. Given an assignment a : V ~ Q+ and an MS~ (V)-knowledge base ~. we denote by ~a the MS~[Q+]-knowledge base which results from~ by replac­ ing each Xi With a(x;).

Let r be a set of constraints for variables in V (say, a set of rational linear inequalities over V or polynomial equations). A knowledge base ~ over MS~ [V] is said to be satisfiable relative to r if there exists an asSignment a such that

• the a(x;) give a solution tor and
• ~a is satisfiable.

Here are two simple examples:

Example 9. (1) r consists of equalities Xi = a;, where a; E Q+. Then a knowledge base ~ over MS~ [V] is sat­ isfiable relative to r iff the knowledge base ~a is satisfiable for a: x; t-t a;. Thus, in this case ~a is a usual MS~(Q+]­ knowledge base considered in the previous sections. -

1. r consists of inequalities x; < x j, so that no absolute values for distances are fixed, and to satisfy ~ we first have to find a solution (assignment) a tor and then check whether ~a is satisfiable.

To illustrate the expressive power of the new language, we will use the following notation: given set terms s1 and s2 , denote by d(s1 , s2 ) = x the set of two MS~ (V]-formulas 81 n ::J:Sx Sz -j:. ..1. and 81 n ::J<x Sz :::::: ..1. (sayin-g that the dis­ tance between s1 and s2 is x). Then we can state that the dis­ tance between Russia and the UK is larger than the distance between Russia and Germany:

Incomplete knowledge can also be expressed by using inter­ val constraints a1 :::; x :::; a2 , where x is a variable occurring in the knowledge base.

Of course, as long as algorithmic properties are not rele­ vant, we can consider arbitrarily complex constraints ron the variables in V. Our main decidability result, however, holds for the case when r consists of a finite set of rational linear inequalities of the form

Namely, we have the following:

Theorem 10. It is decidable whether a given MS~ [V]­ knowledge base ~ is satisfiable relative to a set of rational linear inequalities.

The proof of Theorem 10 is based on a (rather straightfor­ ward) combination of a linear programming technique with the tableau algorithm presented above. The resulting decision procedure is extremely complex. We conjecture, however, that more sophisticated combinations with lower complexity can be developed. Here is one example:

Theorem 11. Suppose that r consists of the 'pure ' strict in­ equalities

and I: is an MS~ [ { x 1 , ... , xn} ]-knowledge base. Then the satisfiability problem for I: relative to r is EXPTIME­ complete.

(In fact I: is satisfiable relative to r iff I:a is satisfiable, where a( xi)= 1 and u(x;) = 1 + n+Li' for 1 < i::; n .)

5 Conclusion

We have introduced and investigated a 'practical' variant of the distance logics from [Sturm et a!., 2000; Kutz et al. , 2003]. Our main achievement is a tableau-based decision procedure similar to those implemented in working descrip­ tion logic systems like FACT and RACER, see [Baader et a!., 2003]. This similarity gives us some grounds to believe that a system based on this tableau procedure (which is cur­ rently being implemented) will be sufficiently fast for 'realis­ tic' applications. As in spatial databases, however, a very im­ portant problem is to integrate the distance logic with other KR&R formalisms. Although in the intended applications the extensions of relevant predicates may strongly depend on the distance measure, usually non-metric attributes and rela­ tions also play a rather significant role (e.g., classifications of proteins, their topological properties). Without an integra­ tion of formalisms taking care of these different aspects of the problem domain one cannot imagine a system powerful enough for real-world applications. Fortunately, a framework for such an integration is already available. The terms of the language MS~ [Q+ ] are constructed from atomic pred­ icates by means or distance and Boolean operators. This makes it possible to treat MS~ [Ql+] as an abstract descrip­ tion system in the sense of [Baader et al., 2002] and com­ bine it in an algorithmically robust way with other effective KR&R formalisms, say, description logics or spatial RCC-8 via E-connections [Kutz et a!., 2002] or fusions [Baader et al., 2002].

Acknowledgements

The work on this paper was supported by the DFG-grant Wo 583/3-3 and by U.K. EPSRC grants no. GR/R45369/0l and GRIR42474/0l. Thanks are due to Anatoli Degtyarev, Ian Hodkinson, Carsten Lutz, and Oliver Kutz for stimulating discussions and remarks on the preliminary versions of the paper.