Gurevich and Neeman introduced Distributed Knowledge Authorization Language (DKAL). The world of DKAL consists of communicating principals computing their own knowledge in their own states. DKAL is based on a new logic of information, the so-called infon logic, and its efficient subsystem called primal logic. In this paper we simplify Kripkean semantics of primal logic and study various extensions of it in search to balance expressivity and efficiency. On the proof-theoretic side we develop cut-free Gentzen-style sequent calculi for the original primal logic and its extensions. This is joint work with Y. Gurevich.
Logic and Computation Seminar
Tuesday, May 17, 2011 - 3:00pm
Lev D. Beklemishev
Steklov Mathematical Institute and Lomonosov Moscow State University