scholarly journals Towards Verified Construction for Planar Class of a Qualitative Spatial Representation

10.29007/zzft ◽  
2018 ◽  
Author(s):  
Sosuke Moriguchi ◽  
Mizuki Goto ◽  
Kazuko Takahashi
Keyword(s):  
Spatial Representation ◽  
Spatial Reasoning ◽  
Base Case ◽  
Proof Assistant ◽  
Qualitative Spatial Reasoning ◽  
Induction Step ◽  
The Third ◽  
Coq Proof Assistant ◽  
Qualitative Spatial Representation

PLCA is a framework for qualitative spatial reasoning, using symbolic objects and relationships between them. To show construction of a PLCA expression, the second and the third authors introduced inductive constructions. They also proved that expressions obtained by inductive constructions are planar (planarity) and planar PLCA expressions can be obtained by inductive constructions (realizability). The former one is proven with Coq proof assistant, but the latter is proven with pen-and-paper.We are currently proving the latter with Coq. We locate some oversights in the original inductive constructions and the proof. In this paper, we report these oversights, re-formalization of inductive constructions and modified proofs. We prove planarity and a base case of realizability with Coq, and induction step of realizability with Coq and pen-and-paper proof.

scholarly journals Qualitative Spatial Representation for the Humanities

2019 ◽  
Vol 13 (1-2) ◽  
pp. 2-27 ◽  
Author(s):  
John G. Stell
Keyword(s):  
Geographical Information Systems ◽  
Spatial Representation ◽  
Spatial Reasoning ◽  
Spatial Relations ◽  
Geographical Information ◽  
Computational Techniques ◽  
Computational Technique ◽  
Qualitative Spatial Reasoning ◽  
Gis Technology ◽  
Geographical Space

‘Qualitative spatial reasoning and representation’ is a range of techniques developed in Artificial Intelligence to meet the need for a computational treatment of qualitative spatial relations. Examples of such relations include ‘next to’, ‘overlapping’, ‘to the left of’, ‘separate from’, ‘including’, and so on. These relations occur within the data found in the spatial humanities, but the computational techniques described here do not appear to have been used in connection with this context. While Geographical Information Systems (GIS) are widely used as a means of visualizing and exploring material in the spatial humanities, GIS technology is acknowledged to be ill-suited to information that is vague, uncertain, ambiguous, imprecise or having other qualities that in a scientific setting could be regarded as imperfections. In the humanities such ‘imperfections’ are of course important, and qualitative spatial relations are one source of data that challenges scientifically based GIS. This article reviews the origin of qualitative spatial reasoning and representation in A. N. Whitehead's mereotopology and argues for exploring how these methods could complement GIS as a computational technique in the humanities. Qualitative representation is applicable to modelling spatial arrangements in many domains, not just geographical space. This is demonstrated through an example of spatial relations in lines of printed text.

Sign in / Sign up

Export Citation Format

Share Document