A proof system for contact relation algebras
type: Item
instance of: scholarly article
title: A proof system for contact relation algebras
zbMATH Open document ID: 0956.03052
DOI: 10.1023/A:1004764610651
published in: Journal of Philosophical Logic
publication date: 2001-03-07T00:00:00Z
review text: A contact relation on a set \(W\) is a reflexive and symmetric relation satisfying a kind of extensionality axiom: if \(xCz \Leftrightarrow yCz\) for all \(z \in W\), then \(x=y\). An intuitive example of a contact structure is provided by a collection of regions in some space, where the contact relation \(C\) is defined by \(xCY \Leftrightarrow x \cap y \neq 0\). However, there is a wide variety of other natural models of contact structures. Relation algebras appeared in spatial reasoning due to \textit{M. Egenhofer} and \textit{J. Sharma} [``Topological consistency'', in: Fifth Internat. Symp. on Spatial Data Handling, Charleston, SC (1992)]. In the paper under review, a sound and complete proof system for relation algebras generated by a contact relation (CRAs, for short) is presented. The primitive notions of the system are contact and identity relations, as well as the relational operators \(\cup, \cap,-,;,\breve{\;}\). Formulas are of the form \(x R y\), where \(R\) is a ``contact expression''. Two more results are obtained: the equational theory of CRAs is undecidable, and the class of contact structures cannot be axiomatised by modal formulas.
reviewed by: Jānis Cīrulis
Mathematics Subject Classification ID: 03G15
Mathematics Subject Classification ID: 51M99
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B60
zbMATH DE Number: 1491205
zbMATH Keywords: contact relation
zbMATH Keywords: mereology
zbMATH Keywords: spatial reasoning
zbMATH Keywords: relation algebras
zbMATH Keywords: equational theory
author: Ivo Düntsch
author: Ewa Orłowska
MaRDI profile type: Publication
cites work: Maintaining knowledge about temporal intervals
cites work: The lattice of varieties of representable relation algebras
cites work: Decision problems for equational theories of relation algebras
cites work: Q4877439
cites work: Connection structures
cites work: Q3325928
cites work: Q5553248
cites work: Small integral relation algebras generated by a partial order
cites work: A necessary relation algebra for mereotopology
cites work: Boolean Algebras with Operators. Part I
cites work: Q4215597
cites work: Q4011727
cites work: Q5688805
cites work: Ontologies for plane, polygonal mereotopology
cites work: A complete axiom system for polygonal mereotopology of the real plane
cites work: Expressivity in polygonal, plane mereotopology
cites work: Dynamic algebras: Examples, constructions, applications
cites work: Q5734410
cites work: Q5582292
cites work: On the calculus of relations
cites work: Q4040000
cites work: Q4342096
cites work: Parts, wholes, and part-whole relations: The prospects of mereotopology
full work available at URL: a:1004764610651
OpenAlex ID: W2060589018
description: scientific article; zbMATH DE number 1491205