A proof system for contact relation algebras

Decidability of theories and sets of sentences (03B25) Other nonclassical logic (03B60) Cylindric and polyadic algebras; relation algebras (03G15) Real and complex geometry (51M99) Logic in artificial intelligence (68T27)

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.

Recommendations

Cites work

Cited in

(12)

This page was built for publication: A proof system for contact relation algebras

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1576385)