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, \(\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.
Chapter PDF
Similar content being viewed by others
References
Beklemishev, L., Gurevich, Y.: Propositional primal logic with disjunction. Journal of Logic and Computation 24(1), 257–282 (2014)
Beklemishev, L., Prokhorov, I.: On computationally efficient subsystems of propositional logic (to appear)
Blass, A., De Caso, G., Gurevich, Y.: An Introduction to DKAL. Microsoft Research technical report, MSR-TR-2012-108 (2012)
Cotrini, C., Gurevich, Y.: Basic primal infon logic. Journal of Logic and Computation (2013)
Cotrini, C., Gurevich, Y.: Transitive primal infon logic. The Review of Symbolic Logic 6, 281–304 (2013)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reason. 31(1), 33–72 (2003)
Gurevich, Y., Neeman, I.: Logic of infons: The propositional case. ACM Trans. Comput. Logic 12(2), 9:1–9:28 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Cotrini, C., Gurevich, Y., Lahav, O., Melentyev, A. (2014). Primal Infon Logic with Conjunctions as Sets. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds) Theoretical Computer Science. TCS 2014. Lecture Notes in Computer Science, vol 8705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44602-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-662-44602-7_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44601-0
Online ISBN: 978-3-662-44602-7
eBook Packages: Computer ScienceComputer Science (R0)