Primal Infon Logic with Conjunctions as Sets
Abstract
Primal infon logic was proposed by Gurevich and Neeman as an efficient 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.
Domains
Origin | Files produced by the author(s) |
---|