Teh Logic of Infons.
Yuri G. Gurevich, Itay Neeman · Bulletin of the European Association for Theoretical Computer Science · 2009
Infons are pieces of information. In our work on the Distributed Knowledge Authorization Language (DKAL), we discovered that the logic of infons is a conservative extension of intuitionistic logic by means of connectives p said and p put where p ranges over principals. We investigate infon logic and a primal fragment of it. In both cases, we develop model theory, prove soundness and completeness, and analyze the computational complexity of the ground multiple derivability (GMD) problem (which of the given ground queries follow form the given ground hypotheses). Our most involved technical result is a linear time algorithm for the GMD problem for the primal infon logic given a constant bound on the quotation depth of the hypotheses. In applications quotation-depth is small. Our result gives rise to a linear time algorithm for the GMD problem for SecPAL, a precursor of DKAL that expresses many important access control scenarios.