A proof system for contact relation algebras (Q1576385)

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.