Primal Infon Logic with Conjunctions as Sets
- Carlos Cotrini ,
- Yuri Gurevich ,
- Ori Lahav ,
- Artem Melentyev
Springer Lecture Notes in Computer Science (2014), TCS 2014, 8th IFIP International Conference on Theoretical Computer Science |
Primal infon logic was proposed by Gurevich and Neeman as an effcient yet expressive logic for policy and trust management. It is a propositional multimodal subintuitionistic logic decidable in linear time. However in that logic the principle of the replacement of equivalents fails. For example, (x ∧ y) → z does not entail (y ∧ x) → z, and similarly w → ((x ∧ y) ∧ z) does not entail w → (x ∧ (y ∧ z)). Imposing the full principle of the replacement of equivalents leads to an NP-hard logic according to a recent result of Beklemishev and Prokhorov. In this paper we suggest a way to regain the part of this principle restricted to conjunction: We introduce a version of propositional primal logic that treats conjunctions as sets, and show that the derivation problem for this logic can be decided in linear expected time and quadratic worst-case time.