Logic of Infons: the Propositional Case

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.