FORMALISING THE LOGIC OF SPATIAL QUALIFICATION USING A QUALITATIVE REASONING APPROACH

Abstract

Spatial qualification problem, an aspect of spatial reasoning, is concerned with the impossibility of knowing an agent‟s presence at a specific location and time. An agent‟s location determines its ability to carry out an action given its known spatial antecedents. There are sparse works on the formalisation of this problem. Qualitative reasoning approach is the most widely used approach for spatial reasoning due to its ability to reason with incomplete knowledge or reduced data set. This approach has been applied to spatial concepts, such as, shapes, sizes, distance and orientation but not spatial qualification. Therefore, this work was aimed at formalising a logical theory for reasoning about the spatial qualification of an agent to carry out an action based on prior knowledge using qualitative reasoning approach. The notions of persistence, discretisation and commutative distance coverage were used as parameters in formalising the concept of spatial qualification. The axioms and derivation rules for the theory were formally represented using quantified modal logic. The formalised theory was compared with standardised systems of axioms: S4 (containing Kripke‟s minimal system K, axioms T and 4) and S5 (containing K,T,4 and axiom B). The characteristics of the domain of the formalised theory were compared with Barcan‟s axioms, and its semantics were described using Kripke‟s Possible World Semantics (PWS) with constant domain across worlds. A proof system for reasoning with the formalised theory was developed using analytical tableau method. The theory was applied to an agent‟s local distribution planning task with set deadline. Cases with known departure time and routes were considered to determine the possibility of an agent‟s presence at a location. From the formalisation, a body of axioms named Spatial Qualification Model (SQM) was obtained. The axioms showed the presence log and reachability of locations as determinants for agent‟s spatial presence. The properties exhibited by the formalised UNIVERSITY OF IBADAN LIBRARY xvii model when examined in light of S4 and S5 systems of axioms were KP1, KP2 (equivalent to axiom K), TP and 4P (equivalent to axioms T and 4 respectively) in an S4 system. The SQM therefore demonstrated the characteristics of an S4 system of axioms but fell short of being an S5 system. Barcan‟s axiom held, confirming constant domain across possible worlds in the formalised model. Explicating the axioms in the SQM using PWS enabled the understanding of tableau proof rules. Through closed tableaux, the SQM was demonstrably semi-decidable in the sense that the possibility of an agent‟s presence at a certain location and time was only provable in the affirmative, while its negation was not. Depending on the route, the application of SQM to the product distribution planning domain resulted in agent‟s feasible availability times, within or outside the set deadline to assess the agent‟s spatial qualification in agreement with possible cases in the planning task. The spatial qualification model specified the spatial presence log and reachability axioms required for reasoning about an agent‟s spatial presence. The model successfully assessed plans of product distribution task from one location to the other for vans‟ availability. Keywords: Spatial qualification model, Quantified modal logic, Tableau proof, Possible world semantics. Word count: 497