# a_logic_of_directions__e84adec0.pdf

A Logic of Directions

Heshan Du1 , Natasha Alechina2 and Anthony G. Cohn3

1University of Nottingham Ningbo China 2Utrecht University, Netherlands 3University of Leeds, UK heshan.du@nottingham.edu.cn, n.a.alechina@uu.nl, a.g.cohn@leeds.ac.uk

We propose a logic of directions for points (LD) over 2D Euclidean space, which formalises primary direction relations east (E), west (W), and indeterminate east/west (Iew), north (N), south (S) and indeterminate north/south (Ins). We provide a sound and complete axiomatisation of it, and prove that its satisﬁability problem is NP-complete.

1 Introduction

This work is motivated by the problem of matching spatial objects represented in different geospatial datasets and verifying the consistency of matching relations. A matching relation states that a spatial object in one dataset is the same as or part of a spatial object in the other dataset. In different datasets, the same real world object is usually represented using different geometries or coordinates. Previously, we proposed a number of qualitative spatial logics (a logic of NEAR and FAR for buffered points, a logic of NEAR and FAR for buffered geometries and a logic of Part and Whole for buffered geometries) which were developed to reason about distance relations between spatial objects from different datasets, tolerating slight differences in their geometric representations [Du et al., 2013; Du and Alechina, 2016]. These spatial logics have been used to validate matching relations regarding the distance relations between spatial objects. The intuition is that two spatial objects which are deﬁnitely close in one dataset cannot be matched to two spatial objects which are deﬁnitely far away in the other dataset. However, these spatial logics do not cover the direction aspect, which is an important dimension of spatial relations. In this work, we propose a new spatial logic for validating matching relations with respect to direction relations between spatial objects. Using the relations deﬁned in the new logic, the following intuition can be formalised: if a spatial object a is deﬁnitely to the east of a spatial object b in one dataset, then the spatial object corresponding to a in the other dataset cannot be deﬁnitely to the west of the spatial object corresponding to b. Consider the case where every spatial object is represented as a single point. We assume that the distance between every pair of corresponding points from different datasets is less than or equal to a positive real number σ. σ is referred to as

a margin of error. The value of σ can be determined empirically by comparing two geospatial datasets representing the same objects, and ﬁnding the largest distortion which exists between any pair of objects. With respect to a point p, if a point q is within the bounding box of the σ-buffer of p (the σ-buffer contains exactly all the points within σ distance of p), then q is considered to be too close to talk about its exact direction. We say that q is not to the north, not to the south, not to the east and not to the west of p. In the logic of NEAR and FAR for buffered points [Du et al., 2013], two points are NEAR, if their distance is within 2σ; two points are FAR, if their distance is greater than 4σ. A gap is left between NEAR and FAR so that two points are not NEAR and not FAR, if their distance is greater than 2σ and within 4σ. Similar to the way in which the relations NEAR and FAR were deﬁned, we will leave some gaps or indeterminate regions between definite directions like deﬁnitely east and deﬁnitely west. E.g. for two points p, q with x coordinates xp, xq, we can deﬁne the three relations deﬁnitely east, not east and not west, and deﬁnitely west, as xp xq > 3σ (p is deﬁnitely to the east of q), σ xp xq σ (p is not to the east and not the west of q) and xp xq < 3σ (p is deﬁnitely to the west of q) respectively. Instead of introducing a constant 3, we introduce another parameter τ > 1 to represent gaps or indeterminate ranges or regions. The parameter τ is referred to as the level of indeterminacy in directions. For points p, q, if xp and xq are within τσ distance, then the direction relation between points p, q are not deﬁnitely east nor deﬁnitely west. Following this initial idea, with respect to a central point p = (0, 0), we divide the 2D Euclidean space into 25 totally or partially bounded regions (see Figure 1). Points in different regions have different direction relations with the central red point p. E.g. for any point q in region 1, q is deﬁnitely to the north and deﬁnitely to the west of p. The question is how to deﬁne the 25 different direction relations formally and provide a sound and complete axiomatisation to reason with them.

Several qualitative spatial or temporal calculi have been developed for formalizing and reasoning about direction or ordering relations [Aiello et al., 2007; Ligozat, 2012]. These include the point calculus [Vilain and Kautz, 1986] which deﬁnes three ordering relations < (less than), > (greater than) and eq (equal) for points in a 1D Euclidean space, Allen s calculus [Allen, 1983], the cardinal direction calculus (CDC) which extends the point calculus to 2D Euclidean

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

12 13 14 15

16 17 18 19 20

21 22 23 24 25

-σ σ τ σ -τ σ

Figure 1: The 2D Euclidean space is divided into 25 totally or partially bounded regions. The red dot in region 13 is the central point p = (0, 0).

space [Ligozat, 1998], the rectangle algebra [Balbiani et al., 1998], the 2n-star calculi which generalize the cardinal direction calculus by introducing a variable n referring to the granularity or the degree of reﬁnement for deﬁning direction relations [Renz and Mitra, 2004], and cardinal direction relations between regions [Goyal and Egenhofer, 1997; Skiadopoulos and Koubarakis, 2004; Skiadopoulos and Koubarakis, 2005]. Beside these formalisms where direction or ordering relations are deﬁned using binary relations, there exist several spatial formalisms which deﬁne direction relations using ternary relations. These spatial formalisms include the LR calculus [Scivos and Nebel, 2004], the ﬂip-ﬂop calculus [Ligozat, 1993], the double-cross calculus [Freksa, 1992], the 5-intersection calculus [Billen and Clementini, 2004], etc., where relations like left, right, after, between, before, etc. are deﬁned. In this paper, we propose a logic of directions for points (LD) over 2D Euclidean space for deﬁning and reasoning about the direction relations shown in Figure 1. Differing from the cardinal direction calculus, in the logic LD, we deﬁne direction relations with respect to the margin of error σ for tolerating slight differences in geometric representations in different geospatial datasets/maps, and the level of indeterminacy in directions τ. Over Euclidean spaces, there exist some sound and complete axiomatisations for spatial formalisms [Szczerba and Tarski, 1979; Balbiani et al., 2007; Tarski, 1959; Tarski and Givant, 1999; Trybus, 2010]; however, none of them considers direction relations. Here we provide a sound and complete axiomatisation for the spatial logic LD which formalises direction relations between points. Some spatial logics, which can encode directions, are undecidable, e.g. the compass logic [Marx and Reynolds, 1999] and Sp PNL [Morales et al., 2007]. The satisﬁability problem of some spatial logics (e.g. Cone [Montanari et al., 2009] and SOSL [Walega and Zawidzki, 2019]) are PSPACEcomplete. Here we show that the satisﬁability problem of LD is NP-complete. The logic LD could be used for checking consistency of same As matches between two real world geospatial datasets (e.g. Ordnance Survey of Great Britain and Open Street Map data) regarding direction information. A sound and complete axiomatisation of LD is an important and useful tool for developing an automated reasoner and performing automated axiom pinpointing [Baader and Pe naloza, 2010] for debugging matches between geospatial objects, as was done, for

d W s W n EW s E d E d N d Nd W d Ns W d Nn EW d Ns E d Nd E s N s Nd W s Ns W s Nn EW s Ns E s Nd E n NS n NSd W n NSs W n NSn EW n NSs E n NSd E s S s Sd W s Ss W s Sn EW s Ss E s Sd E d S d Sd W d Ss W d Sn EW d Ss E d Sd E

Table 1: 25 jointly exhaustive and pairwise disjoint direction relations. Each entry in the table corresponds to the spatially corresponding entry in Figure 1, e.g. n NSs W corresponds to entry 12.

example, in [Du et al., 2015] for the logic of Part and Whole for buffered geometries.

2 A Logic of Directions For Points

We present a logic of directions for points (LD), which deﬁnes six primary direction relations: east (E), west (W), and indeterminate east/west (Iew), north (N), south (S) and indeterminate north/south (Ins). LD is a family of logics LDτ parameterised by a level of indeterminacy parameter τ. Let A be a ﬁnite set of individual names. The language L(LD, A) (we omit A for brevity below) is deﬁned as

φ, ψ := E(a, b) | W (a, b) | Iew(a, b) | N (a, b) | S(a, b) | | Ins(a, b) | φ | φ ψ

where a, b A, φ ψ =def ( φ ψ), φ ψ =def (φ ψ), φ ψ =def (φ ψ) (ψ φ), =def φ φ. We interpret L(LD) over 2D Euclidean models based on the 2D Euclidean space R2. Models of LDτ are called τmodels.

Deﬁnition 1 (2D Euclidean τ-model of LDτ). A 2D Euclidean τ-model M is a tuple (I, σ, τ), where I is an interpretation function which maps each individual name in A to an element of R2, σ R>0 is a margin of error, and τ N>1 refers to the level of indeterminacy in directions. The notion of M |=LD φ (a formula φ of LD is true in τ-model M) is deﬁned as follows:

M |=LD E(a, b) iff xa xb > σ;

M |=LD W (a, b) iff xa xb < σ;

M |=LD Iew(a, b) iff τσ xa xb τσ;

M |=LD N (a, b) iff ya yb > σ;

M |=LD S(a, b) iff ya yb < σ;

M |=LD Ins(a, b) iff τσ ya yb τσ;

M |=LD φ iff M |=LD φ;

M |=LD φ ψ iff M |=LD φ and M |=LD ψ,

where a, b A, I(a) = (xa, ya), I(b) = (xb, yb), φ, ψ are formulas in L(LD).

τ is deﬁned as a natural number rather than a real in order to facilitate the proof of Lemma 5. In practice, an integer τ is always likely to be sufﬁciently expressive. The notions of τ-validity and τ-satisﬁability of LD formulas in 2D Euclidean τ-models are standard. An L(LD) formula is τ-satisﬁable if it is true in some 2D Euclidean τmodel. An L(LD) formula φ is τ-valid (|=τ LD φ) if it is true

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

in all 2D Euclidean τ-models (hence if its negation is not τsatisﬁable). The logic LDτ is the set of all τ-valid formulas of L(LD). As shown by Lemma 1 below, σ is a scaling factor. Lemma 1. For every τ N>1, σ1, σ2 R>0, if an L(LD) formula φ is true in a 2D Euclidean τ-model M = (I, σ1, τ), then it is true in a 2D Euclidean τ-model M = (I , σ2, τ) such that I(a) = (xa, ya) iff I (a) = ( xaσ2

The proof is by straightforward veriﬁcation of truth conditions in Deﬁnition 1. We introduce the following deﬁnitions as syntactic sugar . Deﬁnition 2. deﬁnitely east d E(a, b) =def E(a, b) Iew(a, b) somewhat east s E(a, b) =def E(a, b) Iew(a, b) neither east nor west n EW (a, b) =def E(a, b) W (a, b) somewhat west s W (a,b)=def W (a,b) Iew(a,b) deﬁnitely west d W (a,b)=def W (a,b) Iew(a,b) deﬁnitely north d N (a, b) =def N(a, b) Ins(a, b) somewhat north s N (a, b) =def N (a, b) Ins(a, b) neither north nor south n NS(a, b) =def N (a, b) S(a, b) somewhat south s S(a, b) =def S(a, b) Ins(a, b) deﬁnitely south d S(a,b)=def S(a,b) Ins(a,b) The deﬁnitions of deﬁnite or somewhat direction relations have τ N>1 as a parameter. By Deﬁnitions 1 and 2, M |=LD d E(a, b) iff (xa xb) (τσ, ); M |=LD s E(a, b) iff (xa xb) (σ, τσ]. Let us call (τσ, ) the range of d E(a, b), (σ, τσ] the range of s E(a, b). As τ decreases, the range of d E(a, b) becomes wider, the range of s E(a, b) becomes narrower. If τ is allowed to be 1, then d E(a, b) E(a, b) and s E(a, b) . τ plays a similar role in deﬁning other deﬁnite or somewhat direction relations. There exist 5 5 = 25 jointly exhaustive and pairwise disjoint relations, which can be deﬁned using the primary relations in the logic LD. The 25 direction relations are shown in Table 1. Each of them is deﬁned as a conjunction of one of the relations d W, s W, n EW, s E, d E and one of the relations d N, s N, n NS, s S, d S. These 25 direction relations correspond to the 25 regions shown in Figure 1. For instance, with respect to the central point p, for any point q in region 2, we have d Ns W(q, p) (q is deﬁnitely to the north and somewhat to the west of p). Similar to the logic LD, we could deﬁne a logic over 3D or higher Euclidean space. If we only use east and west (or north and south), we get a logic LD1 over 1D Euclidean space. The soundness, completeness, decidability and complexity results can be obtained similarly. The point calculus and the Cardinal Direction Calculus can be seen as a special case of LD1 and LD respectively, if σ is allowed to be 0. Finally, we observe that there exist different (from LD) extensions of the point calculus and Allen s calculus, for example, introducing the concept of granularity [Cohen-Solal et al., 2015]; a granularity is deﬁned as a sequence of sets of time points where the natural order of the time points are preserved.

3 A Complete Axiomatisation for LD

Here we will ﬁrst describe some results for systems of linear inequalities that are used later in the proofs. Then for each level of indeterminacy τ, we present an axiomatisation (a set of axioms) of LDτ, and prove soundness and completeness of the axiomatisation.

3.1 Deciding Linear Inequalities by Computing Loop Residues We recap the deﬁnitions from [Shostak, 1981]. Let S be a set of linear inequalities of the form ax + by c, where x, y are real variables and a, b, c are reals. Without loss of generality, we assume one of the variables in S, denoted as v0, is special, appearing only with coefﬁcient zero. It is called the zero variable . All other variables in S have nonzero coefﬁcients. The graph for S, denoted as G, is constructed as follows. G contains a vertex for each variable in S and an edge for each inequality, where each vertex is labelled with its associated variable and each edge is labelled with its associated inequality. For example, the edge labelled with ax+by c connects the vertex labelled with x and the vertex labelled with y. Let P be a path through G, given by a sequence v1, . . . , vn+1 of vertices and a sequence e1, . . . , en of edges, n 1. The triple sequence for P is

(a1, b1, c1), (a2, b2, c2), . . . , (an, bn, cn)

where for each i [1, n], aivi + bivi+1 ci is the inequality labelling ei. A path is a loop if its ﬁrst and last vertices are the same. A loop is simple if its intermediate vertices are distinct. P is admissible if for i [1, n 1], bi and ai+1 have opposite signs (one is strictly positive and the other is strictly negative). Deﬁnitions and results that follow apply to admissible paths. The residue inequality of an admissible path P is deﬁned as the inequality obtained from P by applying transitivity to the inequalities labelling its edges. The residue rp of P is deﬁned as the triple (ap, bp, cp),

(ap, bp, cp) = (a1, b1, c1) (a2, b2, c2) (an, bn, cn)

where (a1, b1, c1), . . . , (an, bn, cn) is the triple sequence for P and is the binary operation on triples deﬁned by

(a, b, c) (a , b , c ) = (kaa , kbb , k(ca c b))

where k = a /|a |. The residue inequality of P is a P x + b P y c P , where x, y are the ﬁrst and last vertices of P.

Lemma 2. [Shostak, 1981] Any point (i.e. assignment of reals to variables) that satisﬁes the inequalities labelling on admissible path P also satisﬁes the residue inequality of P.

Let P be an admissible loop with initial vertex x. By Lemma 2, any point satisfying the inequalities along P also satisﬁes a P x + b P x c P . If a P + b P = 0 and cp < 0, then the residue inequality of P is false, and P is called an infeasible loop. Let G be the graph for S. A closure G of G is obtained by adding, for each simple admissible loop P (modulo permutation and reversal) of G, a new edge labelled with the residue inequality of P. A graph is closed if it is a closure of itself.

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

Theorem 1. [Shostak, 1981] Let S be a set of linear inequalities of the form ax+by c, where x, y are real variables and a, b, c are real number constants; let G be a closed graph for S. Then S is satisﬁable iff G has no simple infeasible loop. Theorem 1 is about inequalities of the form ax + by c only. It was extended to include both strict and non-strict inequalities [Shostak, 1981]. We say an admissible path is strict if one or more of its edges is labelled with a strict inequality, i.e. an inequality of the form ax + by < c. Then a strict admissible loop P with residue (a P , b P , c P ) is infeasible, if a P + b P = 0 and c P 0. Corollary 1 is stated for the case where inequalities are of the form x y c or x y < c. Lemma 3 is provided to help readers understand Corollary 1. It follows from the deﬁnition of closed graph. Lemma 3. [Shostak, 1981] Let S be a set of linear inequalities of the form x y c or x y < c, where x, y are real variables and c is a real number constant. Then the graph for S is closed. Corollary 1. [Litvintchouk and Pratt, 1977; Pratt, 1977; Shostak, 1981] Let S be a set of linear inequalities of the form x y c or x y < c, where x, y are real variables and c is a real number constant; G be a graph for S. The set S is not satisﬁable iff G has a simple infeasible loop.

3.2 Axiomatising LD The calculus below (which we will also refer to as LDτ) is sound and complete for LDτ (for any τ). Here, a and b are meta variables which may be instantiated by any individual name. There are 13 axiom schemas (AS 0 to AS 12) and one inference rule. AS 0 All tautologies of classical propositional logic AS 1 W(a, a); AS 2 E(a, b) W (b, a); AS 3 Iew(a, b) Iew(b, a); AS 4 Iew(a, b) ( d E(a, b) d W(a, b)); AS 5 For any n N>1: R1(a0, a1) Rn(an 1, a0) , where for every i such that 1 i n, Ri {W, d W, E, d E}, and number(W)+τ number(d W) = number( E)+ τ number( d E); AS 6 For any n N>0: R1(a0, a1) Rn(an 1, an) W (a0, an), where for every i such that 1 i n, Ri {W, d W, E, d E}, and number(W) + τ number(d W) > number( E) + τ number( d E); AS 7 S(a, a); AS 8 N (a, b) S(b, a); AS 9 Ins(a, b) Ins(b, a); AS 10 Ins(a, b) ( d N(a, b) d S(a, b)); AS 11 For any n N>1: R1(a0, a1) Rn(an 1, a0) , where for every i such that 1 i n, Ri {S, d S, N, d N}, and number(S) + τ number(d S) = number( N) + τ number( d N);

AS 12 For any n N>0: R1(a0, a1) Rn(an 1, an) S(a0, an), where for every i such that 1 i n, Ri {S, d S, N, d N}, and number(S) + τ number(d S) > number( N) + τ number( d N);

MP Modus ponens: φ, φ ψ ψ.

In AS 5, 6, 11 and 12, n is the number of conjuncts in the antecedent of an axiom, number(α) denotes the number of occurrences of α in R1, . . . , Rn. In AS 5 and AS 11, n > 1 because at least two conjuncts are required to make an equality like number(W) + τ number(d W) = number( E) + τ number( d E) true. For AS 5, suppose that n = 4, number(W), number(d W), number( E) and number( d E) are all equal to 1, then an axiom satisfying this is W (a0, a1) d E(a1, a2) E(a2, a3) d W (a3, a0) (the order of the appearance of W, d W, E, d E does not matter). The notion of τ-derivability Γ τ LD φ in the LDτ calculus is standard. An L(LD) formula φ is τ-derivable if τ LD φ; a set of L(LD) formulas. Γ is τ-inconsistent if for some formula φ it τ-derives both φ and φ (otherwise it is τ-consistent).

Theorem 2. For every τ N>1, the LDτ calculus is sound and complete for 2D Euclidean τ-models, i.e. τ LD φ |=τ LD φ (every τ-derivable formula is τ-valid and every τvalid formula is τ-derivable).

For every τ N>1, the proof of soundness (every LD τderivable formula is τ-valid) is by an easy induction on the length of the derivation of φ. By truth deﬁnitions of the direction relations (Deﬁnition 1), AS 1-12 are valid and modus ponens preserves validity. In the rest of this section, we prove completeness. We will actually prove that for every τ N>1, if a ﬁnite set of L(LD) formulas Σ is τ-consistent, then there is a 2D Euclidean τmodel satisfying it. Any ﬁnite set of formulas Σ can be rewritten as a formula ψ that is the conjunction of all the formulas in Σ. Σ is τ-consistent iff ψ is τ-consistent ( τ LD ψ). If there is a 2D Euclidean τ-model M satisfying Σ, then M satisﬁes ψ, hence |=τ LD ψ. Therefore, by showing that if Σ is τ-consistent, then there exists a 2D Euclidean τ-model satisfying it , we show that if τ LD ψ, then |=τ LD ψ . This shows that τ LD φ |=τ LD φ and by contraposition we get completeness. First, we will show that the truth conditions of any set of L(LD) formulas can be expressed as a set of inequalities of the form x1 x2 c or x1 x2 < c.

Lemma 4. An L(LD) formula of the form ( )E(a, b), ( )W(a, b), ( )d E(a, b), ( )d W(a, b), ( )N(a, b), ( )S(a, b), ( )d N(a, b), ( )d S(a, b) is τ-satisﬁable iff an expression of the form x1 x2 c or x1 x2 < c is satisﬁable.

Proof. Deﬁnition 3 shows how to translate such formulas to corresponding inequalities. The translation can be easily veriﬁed to correspond to the truth deﬁnitions in Deﬁnition 1.

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

Deﬁnition 3 (τ-σ-translation). The τ-σ-translation function tr(τ, σ) is deﬁned as follows: tr(τ, σ)(E(a, b)) = (xb xa < σ); tr(τ, σ)(W(a, b)) = (xa xb < σ); tr(τ, σ)(d E(a, b)) = (xb xa < τσ); tr(τ, σ)(d W(a, b)) = (xa xb < τσ); tr(τ, σ)(N(a, b)) = (yb ya < σ); tr(τ, σ)(S(a, b)) = (ya yb < σ); tr(τ, σ)(d N(a, b)) = (yb ya < τσ); tr(τ, σ)(d S(a, b)) = (ya yb < τσ); tr(τ, σ)( φ) = (tr(φ)), where (z1 z2 < c) = (z2 z1 c). The completeness theorem below is proven by rewriting a consistent L(LD) formula φ into disjunctive normal form, where each disjunct φi is τ-satisﬁable, iff a set of linear inequalities Si is satisﬁable, iff the graphs of Si have no simple infeasible loop (Corollary 1 of Theorem 1). We proceed by contradiction, supposing every such graph has a simple infeasible loop P. From P we can obtain L(LD) formulas as conjuncts in φi. Applying the axioms, we show is τderivable from every φi, thus is τ-derivable from φ, which contradicts that φ is τ-consistent. Theorem 3. For every τ N>1, if a ﬁnite set of L(LD) formulas Σ is τ-consistent, then there is a 2D Euclidean τmodel satisfying it.

Proof. Take an arbitrary τ N>1. Suppose a ﬁnite set of L(LD) formulas Σ is τ-consistent. We obtain Σ by rewriting every Iew(a, b) in Σ as d E(a, b) d W(a, b), every Ins(a, b) in Σ as d N(a, b) d S(a, b). By AS 4 and AS 10, Σ and Σ are logically equivalent. Σ can be rewritten as a formula φ that is the conjunction of all the formulas in Σ . We rewrite the L(LD) formula φ into disjunctive normal form φ1 φn (n > 0). Then every literal is of one of the forms E(a, b), W(a, b), d E(a, b), d W(a, b), N(a, b), S(a, b), d N(a, b), d S(a, b), or their negations. Then φ is satisﬁable in a 2D Euclidean τ-model, iff at least one of its disjuncts φi is τ-satisﬁable. We obtain a set of inequalities Si by translating every literal in a disjunct φi as in Deﬁnition 3. Then the inequalities in Si are of the form xa xb < c, xa xb c, ya yb < c or ya yb c, where xa, xb, ya, yb are real variables and c is a real constant. We call variables like xa, xb x variables and variables like ya, yb y variables. Divide Si into two sets Sx i and Sy i , such that Sx i and Sy i contain all the inequalities involving x variables and y variables respectively. By Corollary 1 of Theorem 1, φi is τ-satisﬁable iff the graph Gx i of Sx i has no simple infeasible loop and the graph Gy i of Sy i has no simple infeasible loop. To show there is a 2D Euclidean τ-model satisfying Σ, it is sufﬁcient to show there exists a disjunct φi such that the graph Gx i of Sx i has no simple infeasible loop and the graph Gy i of Sy i has no simple infeasible loop. We prove this by contradiction. Suppose for every disjunct φi, the graph Gx i of Sx i has a simple infeasible loop (Case 1) or the graph Gy i of Sy i has a simple infeasible loop (Case 2). We present the proof for Case 1. Case 2 is similar.

If Gx i has a simple infeasible loop P, then P is either strict or non-strict. Let m denote the sum of the constants c around the loop P. Based on the deﬁnition of infeasible loop, if P is strict, then m 0; otherwise, m < 0. By Deﬁnition 3, if a strict inequality xa xb < c is in Sx i , then c is equal to σ or τσ; if a non-strict inequality xa xb c is in Sx i , then c is equal to σ or τσ, where τ, σ are positive numbers (hence c > 0). If P is non-strict, then all the inequalities in it are of the form xa xb c where c > 0 and the sum of such c is positive. This contradicts the fact that m < 0 for non-strict infeasible loops. Therefore P is strict, hence m 0. We consider the two cases where m = 0 and m < 0 separately. 1. If m = 0, then the sum of the constants around the loop P is equal to 0. Without loss of generality, let us assume P consists of vertices xa0, xa1, ..., xan 1, xa0. Since P is admissible, the linear inequalities in P are of the form (xa0 xa1)?c1, ..., (xan 1 xa0)?cn, where ? is or <, and for every i such that 1 i n, ci is σ, σ, τσ or τσ. Then we translate the linear inequalities in P to formulas as follows. We translate every linear inequality of the form xa xb < σ to W(a, b); every xa xb < τσ to d W(a, b); every xa xb σ to E(a, b); every xa xb τσ to d E(a, b). In this way, from P we obtain a sequence of formulas of the form R1(a0, a1), ..., Rn(an 1, a0), where for every i such that 1 i n, Ri {W, d W, E, d E}. Since the sum of the constants around P is equal to 0, number(W) + τ number(d W) = number( E) + τ number( d E) and n 2. By AS 5, R1(a0, a1) ... Rn(an 1, a0) . By Deﬁnition 3, for every occurrence of W(a, b) in R1(a0, a1) ... Rn(an 1, a0), it or E(b, a) is a conjunct in φi; similarly, for every occurrence of d W(a, b), it or d E(b, a) is a conjunct in φi; for every occurrence of E(a, b), it or W(b, a) is a conjunct in φi; for every occurrence of d E(a, b), it or d W(b, a) is a conjunct in φi. By AS 2, W(a, b) E(b, a). By Deﬁnition 2, AS 2 and AS 3, d W(a, b) d E(b, a). Therefore, is τ-derivable from φi. 2. If m < 0, then the sum of the constants around the loop P is negative. In the same way described above, from P we obtain a sequence of formulas of the form R1(a0, a1), ..., Rn(an 1, a0), where for every i such that 1 i n, Ri {W, d W, E, d E}. Since the sum of the constants around the loop P is negative, number(W) + τ number(d W) > number( E) + τ number( d E) and n 1. By AS 6, R1(a0, a1) ... Rn(an 1, a0) W(a0, a0). By AS 1, W(a0, a0) . Following the same argument above, is τ-derivable from φi. In each case, is τ-derivable from φi. Thus every disjunct φi is not τ-consistent, hence φ is not τ-consistent. This contradicts the fact that Σ is τ-consistent.

4 Decidability and Complexity of LD

We show that for every τ N>1, the satisﬁability problem for LDτ is NP-complete.

Lemma 5. For every τ N>1, let S be a set of linear inequalities obtained by applying the τ-σ-translation function over L(LD) formulas as shown in Deﬁnition 3, where σ = 1; n be the number of variables in S, n > 0. If S is satisﬁable, then it has a solution where for every variable, a rational

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

number t [ nτ, nτ] is assigned to it and the binary representation size of t is polynomial in n and τ.

Proof. Take an arbitrary τ N>1. By Deﬁnition 3, every linear inequality in S is of the form x1 x2 c or x1 x2 < c, where x1, x2 are real variables and c is a real number constant. Let G be a graph for S. By Corollary 1, S is satisﬁable iff G has no simple infeasible loop. The construction of a solution of S is by extending the proof of Theorem 1 [Shostak, 1981] (pp. 777 and 778), which is for non-strict inequalities only, to include both strict and non-strict inequalities. If G has no simple infeasible loop, a solution of S can be constructed as follows. Let v1, . . . , vn 1 be the variables of S other than v0 (the zero variable). We construct a sequence ˆv0, ˆv1, . . . , ˆvn 1 of reals (a solution of S) and a sequence G0, G1, . . . , Gn 1 of graphs inductively: 1. Let ˆv0 = 0 and G0 = G. 2. If ˆvi and Gi have been determined for 0 i < j < n, let

supj = min{ c P

a P | P is an admissible path from vj to v0 in Gj 1 and a P > 0 }

infj = max{ c P

b P | P is an admissible path from v0 to vj in Gj 1 and b P < 0 }

where min = and max = . The range of ˆvj is obtained as follows.

If there is an admissible path P from vj to v0 in Gj 1 such that the residue inequality of P is a P vj < c P , where a P > 0, and c P

a P = supj, then ˆvj < supj, otherwise, ˆvj supj.

If there is an admissible path P from v0 to vj in Gj 1 such that the residue inequality of P is b P vj < c P , where b P < 0, and c P

b P = infj, then ˆvj > infj, otherwise, ˆvj infj.

Instead of letting ˆvj be any real number in the range [Shostak, 1981], we assign a value to ˆvj thus:

if there exists an integer within the range of ˆvj, we assign an integer to ˆvj;

otherwise, the range of ˆvj is of the form infj < ˆvj < supj. Let ˆvj = infj + supj

Let Gj be obtained from Gj 1 by adding two new edges from vj to v0, labelled vj ˆvj and vj ˆvj respectively. To ensure that ˆvj and Gj are well deﬁned, we need the following two claims: 1. For 1 j < n, the range of ˆvj is not empty. 2. For 0 j < n, Gj has no simple infeasible loop. We prove them by induction on j, similar to the proof presented in [Shostak, 1981]. Base case j = 0. 1 holds vacuously; 2 holds since G0 = G. Inductive step Suppose the claim holds for j 1, 0 j 1 < n 1. We will show the claim holds for j. For 1, suppose, to the contrary, that the range of ˆvi is empty. Then in Gj 1, there exist an admissible path P1 from vj to v0, where a P > 0, and an admissible path P2 from v0 to vj, where b P < 0. P1 and P2 forms an admissible loop. By the construction of the range of ˆvi described above, if this range is empty, then the admissible loop formed by P1 and

P2 is infeasible, which contradicts the inductive hypothesis that Gj 1 has no simple infeasible loop. For 2, suppose Gj has a simple infeasible loop P. Since Gj 1 has no such loop, and the loop formed by the two new edges added to Gj 1 to obtain Gj is not infeasible, then P (or its reverse) is of the form P E, where E is one of the two new edges (say the one labelled vj ˆvj; the other case is handled similarly), and P is a path from v0 to vj in Gj 1. Since P is infeasible, if P is strict, ˆvj c P b P , this contradicts that ˆvj > infj, since infj c P

b P ; if P is not strict, ˆvj < c P

b P , this contradicts that ˆvj infj, since infj c P

b P . Q.E.D. Now it remains to show that ˆvj satisﬁes S. Let ax+by c be an inequality in S. We will show that aˆx + bˆy c. We present the case where a > 0 and b < 0. The other cases are similar. Let E be the edge labelled ax + by c in Gn 1. Then, where E1 is the edge labelled ˆx x in Gn 1 and E2 is the one labelled y ˆy, E1EE2 forms an admissible loop. Since Gn 1 has no infeasible loop, E1EE2 is feasible. Hence we have aˆx+bˆy c. The proof for inequalities of the form ax + by < c is similar. By Deﬁnition 3, nτ c P nτ, a P = 1 for supj, b P = 1 for infj. Therefore, supj nτ, infj nτ. Hence every ˆvj (0 j < n) is a rational number in [ nτ, nτ]. Now we will show that the representation size of ˆvj (0 j < n) is polynomial in the size of n and τ. By the construction described above, ˆvj is either an integer in [ nτ, nτ] or obtained by applying the average operation ˆvj = infj + supj

2 . Since τ is a natural number and σ = 1, inf1 and sup1 are integers in [ nτ, nτ]. Also, since 0 < j < n, the number of average operations applied to obtain a ˆvj is at most n. Hence the largest denominator of the values of ˆvj is 2n. Therefore, ˆvj can be represented in a binary notation (bits) of size log(2nτ 2n), which is in O(n + log τ). Hence the representation size of ˆvj is polynomial in n and τ.

Deﬁnition 4. Let φ be an L(LD) formula. Its size s(φ) is deﬁned as follows:

s(R(a, b)) = 3, where R {E, W, Iew, N, S, Ins};

s( φ) = 1 + s(φ);

s(φ ψ) = 1 + s(φ) + s(ψ),

where a, b A, φ, ψ are formulas in L(LD).

The combined size of L(LD) formulas in a set S is deﬁned as the size of the conjunction of all formulas in S.

Theorem 4. For every τ N>1, the satisﬁability problem for a ﬁnite set of L(LD) formulas in a 2D Euclidean τ-model is NP-complete.

Proof. Take an arbitrary τ N>1. NP-hardness is from propositional logic being included in LDτ. To prove that the satisﬁability problem for each LDτ is in NP, we show that if a ﬁnite set of L(LD) formulas Σ is τ-satisﬁable, then we can guess a 2D Euclidean τ-model for Σ and verify that this model satisﬁes Σ, both in time polynomial in the combined size of formulas in Σ and τ. Let s and n denote the combined size of formulas in Σ and the number of individual names in Σ respectively. By Deﬁnition 4, n < s. As σ is a scaling

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

factor, if Σ is τ-satisﬁable, it is τ-satisﬁable in a model where σ = 1. Following the proof of Theorem 3 (ﬁrst paragraph), Σ is satisﬁable in a 2D Euclidean τ-model, iff there exists an Si such that its subsets Sx i and Sy i are both satisﬁable, where Sx i and Sy i are sets of linear inequalities obtained by applying the τ-σ-translation function over L(LD) formulas as shown in Deﬁnition 3. By Lemma 5, if Sx i is satisﬁable, then it has a solution where for every variable, a rational number t [ nτ, nτ] is assigned to it and the representation size of t is in O(n + log τ) (polynomial in n and τ). The same holds for Sy i . Hence for every individual name in Σ, we can guess such a pair of rational numbers for it in O(n+log τ). Thus we can guess a 2D Euclidean τ-model M for Σ in O(n2 + n log τ), in time polynomial in n and τ. To verify that M satisﬁes Σ, we need to check every formula in Σ. For any R(a, b), where R {E, W, Iew, N, S, Ins}, a, b A, checking that R(a, b) is true in M takes O(n + log τ) time by Deﬁnition 1 and applying bit operations. Hense, checking all formulas in Σ takes time polynomial in s and τ.

An alternative decidability/membership of NP proof could use reduction to a ﬁnite set of disjunctive linear relations (DLRs) [Jonsson and B ackstr om, 1998] or a Qbasic formula [Kreutzmann and Wolter, 2014].

5 Conclusion and Future Work

We have introduced a new qualitative logic of directions LD for reasoning about directions in 2D Euclidean space. We have shown it to be sound and complete, and that its decidability is NP-complete. The logic incorporates a margin of error and a level of indeterminacy in directions, that allow it to be used to compare and reason about not perfectly aligned representations of the same spatial objects in different datasets (for example, hand sketches or crowd sourced digital maps). While there have been many spatial calculi previously proposed (as discussed in the introduction), LD is unique in allowing indeterminate directions which we believe are crucial in practice. Moreover, many previous spatial calculi have not been treated to the same theoretical analysis that we do here (i.e. the soundness, completeness and complexity results in this paper). In future work, we plan to combine the logics for qualitative distances [Du et al., 2013; Du and Alechina, 2016] and qualitative directions, and develop reasoners for checking the consistency of matching relations automatically. We also plan to experiment with the logic on actual data in a variety of possible application scenarios. One such scenario could be in spatial data fusion. E.g. consider Figure 2; this shows detections of possible events (such as a karst or an anthropomorphic structure) ahead of a Tunnel Boring Machine (TBM) from sensors mounted on the front of the TBM at different times and spatial locations as the TBM advances through the ground. The detected events will typically appear at different absolute spatial locations because as the TBM advances the sensors are better able to detect and localise features sensors only ever give approximate locations. The challenge is to determine which events at the different time points correspond. The relative positions/directions of the

2 6 4 8 10 12 In front of the Tulips system (m)

T T+1 T+2 T+3

Vertical direction (m)

Figure 2: Detected events (rectangles) and their centroids (circles within the rectangles) at different times ahead of a TBM (from [Wei et al., 2019]; best viewed in colour).

events can be represented using LD. (Of course LD is a logic of points, not regions, but for the purposes of this example we can use the centroid or, probably better, the end points, or just the nearest endpoint since that will have best signal.) In [Wei et al., 2019] simple overlap is used to decide whether two events are the same or not. We hypothesize that it is possible to build a more nuanced system using LD. Events which are d E or d W of each other, may be regarded as discrete events; but if they are n EW then they are candidates to be the same event. By varying σ and τ different levels of tolerance and indeterminacy could be considered and presented to the TBM experts for further analysis and veriﬁcation.

Acknowledgements

This work is supported by the Young Scientist programme of the National Natural Science Foundation of China (NSFC) with a project code 61703218. Anthony Cohn is partially supported by a Fellowship from the Alan Turing Institute, and by the EU Horizon 2020 under grant agreement 825619.

[Aiello et al., 2007] Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors. Handbook of Spatial Logics. Springer, 2007. [Allen, 1983] James F. Allen. Maintaining Knowledge about Temporal Intervals. Communications of the ACM, 26(11):832 843, 1983. [Baader and Pe naloza, 2010] Franz Baader and Rafael Pe naloza. Axiom Pinpointing in General Tableaux. Journal of Logic and Computation, 20(1):5 34, 2010. [Balbiani et al., 1998] Philippe Balbiani, Jean-Franc ois Condotta, and Luis Fari nas del Cerro. A Model for Reasoning about Bidimensional Temporal Relations. In Proc. 6th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 98), pages 124 130, 1998. [Balbiani et al., 2007] Philippe Balbiani, Valentin Goranko, Ruaan Kellerman, and Dimiter Vakarelov. Logical Theories for Fragments of Elementary Geometry. In Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors, Handbook of Spatial Logics, pages 343 428. Springer, 2007. [Billen and Clementini, 2004] Roland Billen and Eliseo Clementini. A Model for Ternary Projective Relations

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)

between Regions. In Proc. 9th Int. Conf. on Extending Database Technology (EDBT), pages 310 328, 2004. [Cohen-Solal et al., 2015] Quentin Cohen-Solal, Maroua Bouzid, and Alexandre Niveau. An Algebra of Granular Temporal Relations for Qualitative Reasoning. In Proc. 24th Int. J. Conf on AI (IJCAI), pages 2869 2875, 2015. [Du and Alechina, 2016] Heshan Du and Natasha Alechina. Qualitative Spatial Logics for Buffered Geometries. Journal of Artiﬁcial Intelligence Research, 56:693 745, 2016. [Du et al., 2013] Heshan Du, Natasha Alechina, Kristin Stock, and Michael Jackson. The Logic of NEAR and FAR. In Proceedings of the 11th International Conference on Spatial Information Theory, volume 8116 of LNCS, pages 475 494. Springer, 2013. [Du et al., 2015] Heshan Du, Hai Nguyen, Natasha Alechina, Brian Logan, Michael Jackson, and John Goodwin. Using Qualitative Spatial Logic for Validating Crowd-Sourced Geospatial Data. In Proceedings of the 27th Conference on IAAI, pages 3948 3953, 2015. [Freksa, 1992] Christian Freksa. Using orientation information for qualitative spatial reasoning. In Proc. Theories and Methods of Spatio-Temporal Reasoning in Geographic Space, Int. Conf. GIS, pages 162 178, 1992. [Goyal and Egenhofer, 1997] Roop K. Goyal and Max J. Egenhofer. The Direction-Relation Matrix: A Representation for Direction Relations between Extended Spatial Objects. In The Annual Assembly and the Summer Retreat of Univ. Consortium for Geog. INf. Systems Science, 1997. [Jonsson and B ackstr om, 1998] Peter Jonsson and Christer B ackstr om. A Unifying Approach to Temporal Constraint Reasoning. Artiﬁcial Intelligence, 102(1):143 155, 1998. [Kreutzmann and Wolter, 2014] Arne Kreutzmann and Diedrich Wolter. Qualitative Spatial and Temporal Reasoning with AND/OR Linear Programming. In Proceedings of the 21st European Conference on Artiﬁcial Intelligence (ECAI), volume 263, pages 495 500, 2014. [Ligozat, 1993] G erard Ligozat. Qualitative Triangulation for Spatial Reasoning. In Proceedings of the 1st International Conference on Spatial Information Theory (COSIT), pages 54 68, 1993. [Ligozat, 1998] G erard Ligozat. Reasoning about Cardinal Directions. Journal of Visual Languages & Computing, 9(1):23 44, 1998. [Ligozat, 2012] G erard Ligozat. Qualitative Spatial and Temporal Reasoning. ISTE Ltd and J. Wiley & Sons, 2012. [Litvintchouk and Pratt, 1977] Steven D. Litvintchouk and Vaughan R. Pratt. A Proof-Checker for Dynamic Logic. In Proc. 5th Int. J. Conf. on AI (IJCAI), pages 552 558, 1977. [Marx and Reynolds, 1999] Maarten Marx and Mark Reynolds. Undecidability of Compass Logic. Journal of Logic and Computation, 9(6):897 914, 1999. [Montanari et al., 2009] Angelo Montanari, Gabriele Puppis, and Pietro Sala. A Decidable Spatial Logic with Cone Shaped Cardinal Directions. In Proc.23rd Int. Workshop

of Computer Science Logic, volume 5771 of LNCS, pages 394 408, 2009. [Morales et al., 2007] Antonio Morales, Isabel Navarrete, and Guido Sciavicco. A new modal logic for reasoning about space: spatial propositional neighborhood logic. Ann. Math. Artif. Intell., 51(1):1 25, 2007. [Pratt, 1977] Vaughan R. Pratt. Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology, 1977. [Renz and Mitra, 2004] Jochen Renz and Debasis Mitra. Qualitative Direction Calculi with Arbitrary Granularity. In Proceedings of the 8th Paciﬁc Rim International Conference on Artiﬁcial Intelligence, pages 65 74, 2004. [Scivos and Nebel, 2004] Alexander Scivos and Bernhard Nebel. The Finest of its Class: The Natural Point-Based Ternary Calculus LR for Qualitative Spatial Reasoning. In Proc. Int. Conf Spatial Cognition, pages 283 303, 2004. [Shostak, 1981] Robert E. Shostak. Deciding Linear Inequalities by Computing Loop Residues. Journal of the ACM, 28(4):769 779, 1981. [Skiadopoulos and Koubarakis, 2004] Spiros Skiadopoulos and Manolis Koubarakis. Composing cardinal direction relations. Artiﬁcial Intelligence, 152(2):143 171, 2004. [Skiadopoulos and Koubarakis, 2005] Spiros Skiadopoulos and Manolis Koubarakis. On the consistency of cardinal direction constraints. Artif. Intell., 163(1):91 135, 2005. [Szczerba and Tarski, 1979] Lesław W. Szczerba and Alfred Tarski. Metamathematical Discussion of Some Afﬁne Geometries. Fundam. Mathematicae, 104:155 192, 1979. [Tarski and Givant, 1999] Alfred Tarski and Steven Givant. Tarski s system of geometry. Bulletin of Symbolic Logic, 5(2):175 214, 1999. [Tarski, 1959] Alfred Tarski. What is Elementary Geometry? In Leon Henkin, Patrick Suppes, and Alfred Tarski, editors, The Axiomatic Method, volume 27 of Studies in Logic and the Foundations of Mathematics, pages 16 29. Elsevier, 1959. [Trybus, 2010] Adam Trybus. An Axiom System for a Spatial Logic with Convexity. In Proc. 19th Europ. Conf. on AI (ECAI), pages 701 706, 2010. [Vilain and Kautz, 1986] Marc B. Vilain and Henry A. Kautz. Constraint Propagation Algorithms for Temporal Reasoning. In Proceedings of the 5th National Conference on Artiﬁcial Intelligence (AAAI-86), pages 377 382, 1986. [Walega and Zawidzki, 2019] Przemyslaw Andrzej Walega and Michal Zawidzki. A Modal Logic for Subject Oriented Spatial Reasoning. In Proc. 26th Int. Symp. on Temporal Representation and Reasoning, volume 147 of LIPIcs, pages 4:1 4:22, 2019. [Wei et al., 2019] Lijun Wei, Muhammad Khan, Owais Mehmood, Qingxu Dou, Carl Bateman, Derek R. Magee, and Anthony G. Cohn. Web-based visualisation for lookahead ground imaging in tunnel boring machines. Automation in Construction, 105:102830, 2019.

Proceedings of the Twenty-Ninth International Joint Conference on Artiﬁcial Intelligence (IJCAI-20)