Как читать нотацию из описания DOT-calculus?

Синтаксис там описан явно в тексте главы 2. Поэтому я думаю, что вопрос о логической нотации (⊢, горизонтальная черта, вот это всё)?

Какой клавиатурой пользуются вимеры?

вот же: github.com/alevchuk/vim-clutch
и ещё можно что-то найти если погуглить, для емакса тоже кто-то сооружал…