Primal logic of information

TL;DR

Primal logic, originating in access control, is a highly efficient logic of information with a systematic transformation from intuitionistic calculus, extended to quantifiers, and has practical applications with bounded quantifiers.

Contribution

The paper introduces Flatting, a systematic transformation from intuitionistic to primal logic, and extends it to quantified primal logic, QPL, with complexity analysis.

Findings

Primal logic has a linear-time decision procedure.

QPL is exponential-time complete, but polynomial-time complete with bounded quantifiers.

Flatting effectively transforms intuitionistic calculus into primal calculus.

Abstract

Primal logic arose in access control; it has a remarkably efficient (linear time) decision procedure for its entailment problem. But primal logic is a general logic of information. In the realm of arbitrary items of information (infons), conjunction, disjunction, and implication may seem to correspond (set-theoretically) to union, intersection, and relative complementation. But, while infons are closed under union, they are not closed under intersection or relative complementation. It turns out that there is a systematic transformation of propositional intuitionistic calculi to the original (propositional) primal calculi; we call it Flatting. We extend Flatting to quantifier rules, obtaining arguably the right quantified primal logic, QPL. The QPL entailment problem is exponential-time complete, but it is polynomial-time complete in the case, of importance to applications (at least to access control), where the number of quantifiers is bounded.