A Logic of Directions

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 definitely close in one dataset cannot be matched to two spatial objects which are definitely 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 defined in the new logic, the following intuition can be formalised: if a spatial object a is definitely to the east of a spatial object b in one dataset, then the spatial object corresponding to a in the other dataset cannot be definitely 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 finding 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 defined, we will leave some gaps or indeterminate regions between definite directions like definitely east and definitely west. E.g. for two points p, q with x coordinates xp, xq, we can define the three relations definitely east, not east and not west, and definitely west, as xp -xq > 3σ (p is definitely 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 definitely 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 definitely east nor definitely 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 definitely to the north and definitely to the west of p. The question is how to define 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 defines 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 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 refinement for defining 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 defined using binary relations, there exist several spatial formalisms which define direction relations using ternary relations. These spatial formalisms include the LR calculus [Scivos and Nebel, 2004], the flip-flop 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 defined.

In this paper, we propose a logic of directions for points (LD) over 2D Euclidean space for defining and reasoning about the direction relations shown in Figure 1. Differing from the cardinal direction calculus, in the logic LD, we define 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 SpPNL [Morales et al., 2007]. The satisfiability 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 satisfiability problem of LD is NP-complete.

The logic LD could be used for checking consistency of sameAs matches between two real world geospatial datasets (e.g. Ordnance Survey of Great Britain and OpenStreetMap 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 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 defines 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 finite set of individual names. The language L(LD, A) (we omit A for brevity below) is defined as

We interpret L(LD) over 2D Euclidean models based on the 2D Euclidean space R2 . Models of LDτ are called τmodels.

Definition 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 defined as follows:

τ is defined 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 sufficiently expressive.

The notions of τ-validity and τ-satisfiability of LD formulas in 2D Euclidean τ-models are standard. An L(LD) formula is τ-satisfiable if it is true in some 2D Euclidean τmodel. An L(LD) formula φ is τ-valid (|=τLD φ) if it is true in all 2D Euclidean τ-models (hence if its negation is not τsatisfiable). 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 σ1 , yaσ2 σ1 ).

The proof is by straightforward verification of truth conditions in Definition 1.

We introduce the following definitions as 'syntactic sugar'. Definition 2.

somewhat east sE(a, b) =def E(a, b) ∧ Iew(a, b)

neither east nor west nEW(a, b) =def ¬E(a, b)∧

¬W (a, b)

somewhat west sW(a,b)=def W(a,b) ∧Iew(a,b)

somewhat north sN(a, b) =def N(a, b) ∧ Ins(a, b)

neither north nor south nNS(a, b) =def ¬N(a, b)∧

¬S (a, b)

somewhat south sS(a, b) =def S(a, b) ∧ Ins(a, b)

definitely south dS(a,b)=def S(a,b)∧¬Ins(a,b)

The definitions of definite or somewhat direction relations have τ ∈ N>1 as a parameter. By Definitions 1 and 2, M |=LD dE(a, b) iff (xa - xb) ∈ (τσ,∞); M |=LD sE(a, b) iff (xa - xb) ∈ (σ, τσ]. Let us call (τσ,∞) the range of dE(a, b), (σ, τσ] the range of sE(a, b). As τ decreases, the range of dE(a, b) becomes wider, the range of sE(a, b) becomes narrower. If τ is allowed to be 1, then dE(a, b) ≡ E(a, b) and sE(a, b) ≡ ⊥. τ plays a similar role in defining other definite or somewhat direction relations.

There exist 5 × 5 = 25 jointly exhaustive and pairwise disjoint relations, which can be defined using the primary relations in the logic LD. The 25 direction relations are shown in Table 1. Each of them is defined as a conjunction of one of the relations dW, sW, nEW, sE, dE and one of the relations dN, sN, nNS, sS, dS. 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 dNsW(q, p) (q is definitely to the north and somewhat to the west of p).

Similar to the logic LD, we could define 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 defined as a sequence of sets of time points where the natural order of the time points are preserved.

3 AComplete Axiomatisation for LD

Here we will first 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 definitions 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 coefficient zero. It is called the 'zero variable'. All other variables in S have nonzero coefficients.

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

where for each i ∈ [1, n], aivi +bivi+1 ≤ ci is the inequality labelling ei. A path is a loop if its first 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). Definitions and results that follow apply to admissible paths.

The residue inequality of an admissible path P is defined as the inequality obtained from P by applying transitivity to the inequalities labelling its edges. The residue rp of P is defined as the triple (ap, bp, cp),

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

where k = a′ /|a′ |. The residue inequality of P is aPx + bP y ≤ cP , where x, y are the first and last vertices of P .

Lemma 2. [Shostak, 1981] Any point (i.e. assignment of reals to variables) that satisfies the inequalities labelling on admissible path P also satisfies 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 satisfies aPx + bPx ≤ cP . If aP + bP = 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.

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 satisfiable 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 (aP , bP , cP ) is infeasible, if aP + bP = 0 and cP ≤ 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 definition 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 satisfiable 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) ↔ (¬dE(a, b) ∧¬dW(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, dW, ¬E, ¬dE}, and number(W )+τ ∗number(dW ) = number(¬E)+ τ ∗ number(¬dE);

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, dW, ¬E, ¬dE}, and number(W) + τ ∗ number(dW) > number(¬E) + τ ∗ number(¬dE);

• 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) ↔ (¬dN(a, b) ∧¬dS(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, dS, ¬N, ¬dN}, and number(S) + τ ∗ number(dS) = number(¬N) + τ ∗ number(¬dN );

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, dS, ¬N, ¬dN}, and number(S) + τ ∗ number(dS) > number(¬N) + τ ∗ number(¬dN);

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(dW) = number(¬E) + τ ∗ number(¬dE) true. For AS 5, suppose that n = 4, number(W), number(dW), number(¬E) and number(¬dE) are all equal to 1, then an axiom satisfying this is W (a0 , a1 ) ∧ ¬dE (a1 , a2 ) ∧ ¬E (a2 , a3 ) ∧ dW (a3 , a0 ) → ⊥ (the order of the appearance of W, dW, ¬E, ¬dE 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 definitions of the direction relations (Definition 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 finite set of L(LD) formulas Σ is τ-consistent, then there is a 2D Euclidean τmodel satisfying it. Any finite 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 satisfies ψ, 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), (¬)dE(a, b), (¬)dW(a, b), (¬)N(a, b), (¬)S(a, b), (¬)dN(a, b), (¬)dS(a, b) is τ-satisfiable iff an expression of the form x1 - x2 ≤ c or x1 - x2 < c is satisfiable.

Proof. Definition 3 shows how to translate such formulas to corresponding inequalities. The translation can be easily verified to correspond to the truth definitions in Definition 1.

Definition 3 (τ-σ-translation). The 'τ-σ-translation' function tr(τ, σ) is defined as follows:

The completeness theorem below is proven by rewriting a consistent L(LD) formula φ into disjunctive normal form, where each disjunct φi is τ-satisfiable, iff a set of linear inequalities Si is satisfiable, 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 finite set of L(LD) formulas Σ is τ-consistent, then there is a 2D Euclidean τmodel satisfying it.

Proof. Take an arbitrary τ ∈ N>1. Suppose a finite set of L(LD) formulas Σ is τ-consistent. We obtain Σ′ by rewriting every Iew(a, b) in Σ as ¬dE(a, b) ∧ ¬dW(a, b), every Ins(a, b) in Σ as ¬dN(a, b) ∧ ¬dS(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), dE(a, b), dW(a, b), N(a, b), S(a, b), dN(a, b), dS(a, b), or their negations. Then φ is satisfiable in a 2D Euclidean τ-model, iff at least one of its disjuncts φi is τ-satisfiable. We obtain a set of inequalities Si by translating every literal in a disjunct φi as in Definition 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 τ -satisfiable iff the graph Gxi of Sx i has no simple infeasible loop and the graph Gyi of Sy i has no simple infeasible loop. To show there is a 2D Euclidean τ-model satisfying Σ, it is sufficient to show there exists a disjunct φi such that the graph Gxi of Sx i has no simple infeasible loop and the graph Gyi of Sy i has no simple infeasible loop.

We prove this by contradiction. Suppose for every disjunct φi, the graph Gxi of Sx i has a simple infeasible loop (Case 1) or the graph Gyi of Sy i has a simple infeasible loop (Case 2). We present the proof for Case 1. Case 2 is similar.

If Gxi 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 definition of infeasible loop, if P is strict, then m ≤ 0; otherwise, m < 0. By Definition 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 dW(a, b); every xa-xb ≤ σ to ¬E(a, b); every xa-xb ≤ τσ to ¬dE(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, dW, ¬E, ¬dE}. Since the sum of the constants around P is equal to 0, number(W) + τ ∗ number(dW) = number(¬E) + τ ∗ number(¬dE) and n ≥ 2. By AS 5, R1(a0, a1) ∧ ... ∧ Rn(an-1, a0) → ⊥. By Definition 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 dW(a, b), it or dE(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 ¬dE(a, b), it or ¬dW(b, a) is a conjunct in φi. By AS 2, W(a, b) ↔ E(b, a). By Definition 2, AS 2 and AS 3, dW(a, b) ↔ dE(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, dW, ¬E, ¬dE}. Since the sum of the constants around the loop P is negative, number(W) + τ ∗ number(dW) > number(¬E) + τ ∗ number(¬dE) 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 satisfiability 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 Definition 3, where σ = 1; n be the number of variables in S, n > 0. If S is satisfiable, then it has a solution where for every variable, a rational 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 Definition 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 satisfiable 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{ cP aP | P is an admissible path from vj to v0 in Gj-1 and aP > 0 }

infj = max{ cP bP | P is an admissible path from v0 to vj in Gj-1 and bP < 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 aPvj < cP , where aP > 0, and cP aP = 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 bPvj < cP , where bP < 0, and cP bP = 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 2 .

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 defined, 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 aP > 0, and an admissible path P2 from v0 to vj, where bP < 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 ≤ cP′ bP′ , this contradicts that ˆ vj > infj, since infj ≥ cP′ bP′ ; if P ′ is not strict, ˆ vj < cP′ bP′ , this contradicts that ˆ vj ≥ infj, since infj ≥ cP′ bP′ . Q.E.D.

Now it remains to show that ˆ vj satisfies 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 Definition 3, -nτ ≤ cP ≤ nτ , aP = 1 for supj , bP = -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 τ.

Definition 4. Let φ be an L(LD) formula. Its size s(φ) is defined 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 defined as the size of the conjunction of all formulas in S.

Theorem 4. For every τ ∈ N>1, the satisfiability problem for a finite 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 satisfiability problem for each LDτ is in NP, we show that if a finite set of L(LD) formulas Σ is τ-satisfiable, then we can guess a 2D Euclidean τ-model for Σ and verify that this model satisfies Σ, 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 Definition 4, n < s. As σ is a scaling factor, if Σ is τ-satisfiable, it is τ-satisfiable in a model where σ = 1.

Following the proof of Theorem 3 (first paragraph), Σ is satisfiable in a 2D Euclidean τ-model, iff there exists an Si such that its subsets Sx i and Sy i are both satisfiable, where Sx i and Sy i are sets of linear inequalities obtained by applying the τ-σ-translation function over L(LD) formulas as shown in Definition 3. By Lemma 5, if Sx i is satisfiable, 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 satisfies Σ, 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 Definition 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 finite set of disjunctive linear relations (DLRs) [Jonsson and B¨ackstr¨om, 1998] or a Qbasic formula [Kreutzmann and Wolter, 2014].

5 Conclusion and FutureWork

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 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 dE or dW of each other, may be regarded as discrete events; but if they are nEW 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 verification.

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.