Complete axiomatization of relation algebras without ${}^-$ and $\top$ I'm working on a more thorough algebraic treatment of delta modeling. Briefly, deltas are syntactic entities that can modify products (as in 'software products'). They actually represent relations on products, so that they could be both partially defined and non-deterministic.

I've been looking into relation algebras. For obvious reasons they seemed like a good place to start.

A relation algebra is a structure $(S, \vee, \wedge, {}^-, \bot, \top, \cdot, \epsilon, {}^\smallsmile)$ with disjunction, conjunction, negation, an empty element, a complete element, composition, a neutral element and converse. Semantically they correspond to the relation operations $(2^{P^2}, \cup, \cap, {}^{\mathsf C}, \varnothing, P^2, \circ, \mathrm{id}_P, {}^{-1})$.

But this is more expressiveness than I need. If I could just remove negation $^-$ and the complete element $\top$, the operations that remain have sensible interpretations for delta modeling. Moreover, it seems that in contrast to $^-$ and $\top$, the operations that remain are in a sense 'constructive' (though I'm not sure the term is apt here), since their meaning does not depend on the description of the full set of products $P$.

Has the structure $(S, \vee, \wedge, \bot, \cdot, \epsilon, {}^\smallsmile)$ been studied? Is there a complete axiomatization for it (with respect to the behavior of the corresponding relation operations)? Does it have a decidable theory?



Edit: I've discovered the work of Hajnal Andréka and Szabolcs Mikulás. In particular the article entitled Axiomatizability of positive algebras of binary relations (a PDF version can be found with Google).

This article seems to summarize some of the results I need. If I understand correctly, the exact structure I describe is not finitely axiomatizable, but it will be if I also remove either $\wedge$, $\cdot$ or ${}^\smallsmile$. Moreover, any signature without that combination, but with $\cdot$ and either $\vee$ or $\wedge$, is finitely axiomatizable.

However, I'm not well-versed enough yet in abstract algebra to write up a coherent answer myself. For example, I don't understand why the presence of $\vee$ or $\wedge$ is required. If I omit both, aren't we simply in monoid territory? And I also still don't know about a decidable theory.

So I would still appreciate it if someone with more experience could write up an answer, preferably one that is easier to understand for the layman than the above cited article.
The equational theory of the signature $S=\{\vee,\wedge,.,\epsilon,^\smile\}$ is decidable. See this paper by Andréka and Bredikhin.
The idea is to associate to every term $t$ over $S$ a graph $G_t$. Then Andréka and Bredikhin show that two terms $t$ and $u$ are equivalent iff there is a graph homomorphism from $G_t$ to $G_u$ and a graph homomorphism from $G_u$ to $G_t$. Testing graph homomorphism between finite graphs is decidable, hence the equational theory is also decidable.
The equational theory of $S$ is not finitely axiomatizable, due to the paper of Andréka and Mikulas you have cited. However, contrarily to what is claimed in this paper, the restrictions of the signature to, say, $\{., \cap, \epsilon\}$ is not finitely axiomatizable, as shown in this paper.