Qualitative Spatial Reasoning With Super-Intuitionistic Logics

Topology is used in many applications that may benefit from the automation of spatial reasoning, notably in geographic information systems and in graphics. Reasoning about topology is known to be intrinsically complex, and difficult to be dealt with by a machine. Qualitative formalisms for spatial reasoning, region-based approaches to mereotopology, encodings based on non-classical logics are some of the possible answers that have emerged in connection with this problem. The present analysis is based on the well-known topological semantics of intuitionistic logic. That semantics is considered here from the point of view of the representation of spatial knowledge, and accordingly extended, in order to allow more naturally the expression of simple topological descriptions. Special attention is given to the formal modelling of digital representation, to the logical encoding of connectivity relations, to the concepts of granularity and dimension. The formalisations that are investigated are based on some extensions of intuitionistic propositional logic. These can be obtained by adding to the basic logic propositional quantifiers, intuitionistic modalities and intermediate axioms. A proof-checking tool for some of these logics has been developed, by formalising them in Isabelle-HOL, an interactive theorem-prover based on classical higher-order logic. A partial decidability result is given for an extension of intuitionistic second-order propositional logics, together with an account of its mechanisation.