TRANSITIVE PRIMAL INFON LOGIC

Primal infon logic was introduced in 2009 in connection with access control. In addition to traditional logic constructs, it contains unary connectives p said indispensable in the intended access control applications. Propositional primal infon logic is decidable in linear time, yet suffices for man...

Full description

Saved in:
Bibliographic Details
Published in:The review of symbolic logic 2013-06, Vol.6 (2), p.281-304
Main Authors: COTRINI, CARLOS, GUREVICH, YURI
Format: Article
Language:English
Subjects:
Access control
Algorithms
Logic
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Primal infon logic was introduced in 2009 in connection with access control. In addition to traditional logic constructs, it contains unary connectives p said indispensable in the intended access control applications. Propositional primal infon logic is decidable in linear time, yet suffices for many common access control scenarios. The most obvious limitation on its expressivity is the failure of the transitivity law for implication: $x \to y$ and $y \to z$ do not necessarily yield $x \to z$. Here we introduce and investigate equiexpressive “transitive” extensions TPIL and TPIL* of propositional primal infon logic as well as their quote-free fragments TPIL0 and TPIL0* respectively. We prove the subformula property for TPIL0* and a similar property for TPIL*; we define Kripke models for the four logics and prove the corresponding soundness-and-completeness theorems; we show that, in all these logics, satisfiable formulas have small models; but our main result is a quadratic-time derivation algorithm for TPIL*.
ISSN:1755-0203
1755-0211
DOI:10.1017/S1755020312000366