%0 Conference Proceedings
%T Primal Infon Logic with Conjunctions as Sets
%+ Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology  [Zürich] (ETH Zürich)
%+ Microsoft Research [Redmond]
%+ Tel Aviv University (TAU)
%+ Ural Federal University [Ekaterinburg] (UrFU)
%A Cotrini, Carlos
%A Gurevich, Yuri
%A Lahav, Ori
%A Melentyev, Artem
%Z Part 2: Track B: Logic, Semantics, Specification and Verification
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 8th IFIP International Conference on Theoretical Computer Science (TCS)
%C Rome, Italy
%Y Josep Diaz
%Y Ivan Lanese
%Y Davide Sangiorgi
%I Springer
%3 Theoretical Computer Science
%V LNCS-8705
%P 236-249
%8 2014-09-01
%D 2014
%R 10.1007/978-3-662-44602-7_19
%Z Computer Science [cs]Conference papers
%X 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, $\left(x \land y\right) \to z$ does not entail $\left(y \land x\right) \to z$, and similarly $w \to \left(\left(x \land y\right)\land z\right)$ does not entail $w \to \left(x \land \left(y \land z\right)\right)$. 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.
%G English
%Z TC 1
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01402046/document
%2 https://inria.hal.science/hal-01402046/file/978-3-662-44602-7_19_Chapter.pdf
%L hal-01402046
%U https://inria.hal.science/hal-01402046
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-LNCS-8705
%~ IFIP-TCS
%~ IFIP-WG2-2