• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Препринт

Propositional primal logic with disjunction

Beklemishev L. D., Gurevich Y.
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 ecient 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 eciency. On the proof-theoretic side we develop cut-free Gentzen-style sequent calculi for the original primal logic and its extensions.