Contact logics are modal logic that is developed for reasoning about region-based theories of space. We develope a tableaux approach for contact logics interpreted over intervals (CLIOI) on the reals. For obtaining sound and complete tableaux-based decision procedures, the main technical tool is the semantic tableaux approach. We use intensively the following concepts: tableaux methods, termination of tableaux methods, saturated tableaux, termination theorem, soundness theorem, truth lemma, and completeness theorem.

We continue the work of [1, 2, 3] by analyzing the equivalence relation of bi-embeddability on various classes of countable planes, most notably the class of countable non-Desarguesian projective planes. We use constructions of the author from [13] to show that these equivalence relations are invariantly universal, in the sense of [3], and thus in particular complete analytic. We also introduce a new kind of Borel reducibility relation for standard Borel G-spaces, which requires the preservation of stabilizers, and explain its connection with the notion of full embeddings commonly considered in category theory.