Logic of Infons: the Propositional Case

  • Yuri Gurevich ,
  • Itay Neeman

MSR-TR-2011-90 |

The version available here corrects an oversight in the paper. An earlier version of the paper was published in Bulletin of Euro. Assoc. for Theor. Computer Science 98 (2009).

Infons are statements viewed as containers of information (rather then representations of truth values). The logic of infons turns out to be a conservative extension of logic known as constructive or intuitionistic. Distributed Knowledge Authorization Language uses additional unary connectives “p said” and “p implied” where p ranges over principals. Here we investigate infon logic and a narrow but useful primal fragment of it. In both cases, we develop model theory and analyze the derivability problem: Does the given query follow from the given hypotheses? Our more involved technical results are on primal infon logic. We construct an algorithm for the multiple derivability problem: Which of the given queries follow from the given hypotheses? Given a bound on the quotation depth of the hypotheses, the algorithm runs in linear time. We quickly discuss the significance of this result for access control.