Basic Primal Infon Logic

Primal infon logic (PIL) was introduced in 2009 in the framework of policy and trust management. In the meantime, some generalizations appeared, and there have been some changes in the syntax of the basic PIL. This paper is on the basic PIL, and one of our purposes is to “institutionalize” the changes. We prove a small-model theorem for the propositional fragment of basic primal infon logic (PPIL), give a simple proof of the PPIL locality theorem, and present a linear-time decision algorithm (announced earlier) for PPIL in a form convenient for generalizations. For the sake of completeness, we cover the universal fragment of basic primal infon logic. We wish that this paper becomes a standard reference on basic primal infon logic.

A special issue devoted to Arnon Avron.

First published online July 22, 2013, doi:10.1093/logcom/ext021 Preliminary version: Microsoft Research technical report MSR-TR-2012-88.