White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Logical representations for automated reasoning about spatial relationships

Bennett, Brandon (1997) Logical representations for automated reasoning about spatial relationships. PhD thesis, University of Leeds.

[img]
Preview
Text
bennett_b.pdf

Download (1542Kb)

Abstract

This thesis investigates logical representations for describing and reasoning about spatial situations. Previously proposed theories of spatial regions are investigated in some detail - especially the 1st-order theory of Randell, Cui and Cohn (1992). The difficulty of achieving effective automated reasoning with these systems is observed. A new approach is presented, based on encoding spatial relations in formulae of 0-order ('propositional') logics. It is proved that entailment, which is valid according to the standard semantics for these logics, is also valid with respect to the spatial interpretation. Consequently, well-known mechanisms for propositional reasoning can be applied to spatial reasoning. Specific encodings of topological relations into both the modal logic S4 and the intuitionistic propositional calculus are given. The complexity of reasoning using the intuitionistic representation is examined and a procedure is presented with is shown to be of O(n3) complexity in the number of relations involved. In order to make this kind of representation sufficiently expressive the concepts of model constraint and entailment constraint are introduced. By means of this distinction a 0-order formula may be used either to assert or to deny that a certain spatial constraint holds of some situation. It is shown how the proof theory of a 0-order logical language can be extended by a simple meta-level generalisation to accommodate a representation involving these two types of formula. A number of other topics are dealt with: a decision procedure based on quantifier elimination is given for a large class of formulae within a 1st-order topological language; reasoning mechanisms based on the composition of spatial relations are studied; the non-topological property of convexity is examined both from the point of view of its 1st-order characterisation and its incorporation into a 0-order spatial logic. It is suggested that 0-order representations could be employed in a similar manner to encode other spatial concepts.

Item Type: Thesis (PhD)
Additional Information: Supplied directly by the School of Computing, University of Leeds.
Academic Units: The University of Leeds > Faculty of Engineering (Leeds) > School of Computing (Leeds)
Identification Number/EthosID: uk.bl.ethos.528714
Depositing User: Dr L G Proll
Date Deposited: 28 Feb 2011 14:39
Last Modified: 07 Mar 2014 11:23
URI: http://etheses.whiterose.ac.uk/id/eprint/1271

Actions (repository staff only: login required)