Loop-check elimination for non-transitive distributed knowledge logic

Abstract

A non-transitive distributed knowledge logic T_nD, obtained from multi-modal logic T_n by adding distributed knowledge operator, is considered. Sound and complete loop-check-free sequent calculus for this logic is proposed. Termination of derivations in proposed calculus is justified.