We give an overview of decidability results for modal logics having a binary modality. We put an emphasis on the demonstration of proof-techniques, and hope that this will also help in finding the borderlines between decidable and undecidable fragments of usual first-order logic.

It is shown that both classical and intuitionistic propositional logics of an associative binary modality are undecidable. The proof is based on the deduction theorem for these logics.