Primal Infon Logic: Derivability in Polynomial Time

摘要

Primal infon logic (PīL), introduced by Gurevich and Neeman in 2009, is a logic for authorization in distributed systems. It is a variant of the (→,Λ)-fragment of intuitionistic modal logic. It presents many interesting technical challenges - one of them is to determine the complexity of the derivability problem. Previously, some restrictions of propositional PIL were proved to have a linear time algorithm, and some extensions have been proved to be PSPACE-complete. In this paper, we provide an 0(N3) algorithm for derivability in propositional PIL. The solution involves an interesting interplay between the sequent-calculus formulation (to prove the subfor- mula property) and the natural deduction formulation of the logic, (based on which we provide an algorithm for the derivability problem).