Please enter verification code
Automated Proof Search System for Logic of Correlated Knowledge
American Journal of Mathematical and Computer Modelling
Volume 5, Issue 2, June 2020, Pages: 29-42
Received: Oct. 4, 2019; Accepted: Mar. 2, 2020; Published: Apr. 14, 2020
Views 426      Downloads 111
Haroldas Giedra, Institute of Computer Science, Vilnius University, Vilnius, Lithuania
Romas Alonderis, Institute of Data Science and Digital Technologies, Vilnius University, Vilnius, Lithuania
Article Tools
Follow on us
Logic of correlated knowledge is one of the latest development in logical systems, allowing to handle information about quantum systems. Quantum system may consist of one or more elementary particles. Associating agent to each particle, we get multi-agent system, where agents can perform observations and get results. Allowing communication between agents, correlations such as quantum entanglement can be extracted. This can not be done by traditional epistemic logic or logic of distributed knowledge. Our main scientific result is proof search system GS-LCK-PROC for logic of correlated knowledge, which lets to reason about knowledge automatically. The core of the system is the sequent calculus GS-LCK with the properties of soundness, completeness, admissibility of cut and structural rules, and invertibility of all rules. The ideas of semantic internalization are used to get such properties for the calculus. The calculus provides convenient means for backward proof search and decision procedure for logic of correlated knowledge. The procedure generates a finite model for each sequent. As a result we get termination of the proof search and decidability of logic of correlated knowledge.
Logic of Correlated Knowledge, Sequent Calculus, Automated Proof System, Decidability, Soundness, Completeness, Admissibility of the Cut Rule
To cite this article
Haroldas Giedra, Romas Alonderis, Automated Proof Search System for Logic of Correlated Knowledge, American Journal of Mathematical and Computer Modelling. Vol. 5, No. 2, 2020, pp. 29-42. doi: 10.11648/j.ajmcm.20200502.11
Copyright © 2020 Authors retain the copyright of this article.
This article is an open access article distributed under the Creative Commons Attribution License ( which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
D. Aerts. Description of compound physical systems and logical interaction of physical systems. Current Issues on Quantum Logic, 8: 381C405, 1981.
A. Araujo and M. Finger. A formal system for quantum communication environments. VIII - Brazilian National Meeting for Artificial Intelligence, pages 1C11, 2011.
A. Baltag and S. Smets. Correlated knowledge: an epistemic-logic view on quantum entanglement. International Journal of Theoretical Physics, 49 (12): 3005C3021, 2010.
A. Baltag and S. Smets. Logics of informational interactions. Journal of Philosophical Logic, 44: 595C 607, 2015.
A. Baltag and S. Smets. Modeling correlated information change: from conditional beliefs to quantum conditionals. Soft computing, 21 (6): 1523C1535, 2017.
G. Battilotti. Characterization of quantum states in predicative logic. Int. J. Theor. Phys., 50: 3669C3681, 2011.
G. Birkhoff and J. von Neumann. The logic of quantum mechanics. Annals of Mathematics, 37: 823C843, 1936.
F. Boge. Quantum information vs. epistemic logic: An analysis of the frauchiger-renner theorem. Foundations of Physics, 49 (10): 1143C1165, 2019.
B. Coecke, C. Heunen, and A. Kissinger. Compositional quantum logic. Computation, Logic, Games, and Quantum Foundations, pages 21C36, 2013.
R. Fagin, J. Y. Halpern, and M. Y. Vardi. What can machines know? on the properties of knowledge in distributed systems. Journal of the ACM, 39 (2): 328C376, 1992.
G.Gentzen. Untersuchungenuberdaslogischeschliesen. i. Mathematische Zeitschrift, 39 (2): 176C210, 1934.
S. Kripke. Semantical analysis of modal logic i. normal propositional calculi. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 9: 67C96, 1963.
G. Mackey. Quantum mechanics and hilbert space. American Mathematical Monthly, 64 (2): 45C57, 1957.
G. Mackey. The mathematical foundations of quantum mechanics. W.A. Benjamin, NY, 1963.
S. Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34 (5): 507C544, 2005.
S. Negri and J. von Plato. Structural Proof Theory. Cambridge University Press, 2001.
N. Nurgalieva and L. del Rio. Inadequacy of modal logic in quantum settings. EPTCS 287, pages 267C297, 2019.
C. Piron. Foundations of quantum physics. W.A. Benjamin Inc., Massachusetts, 1976.
C. Randall and D. Foulis. Tensor products of quantum logics do not exist. Notices Amer. Math. Soc., 26 (6), 1979.
S. Smets. Logic and quantum physics. Journal of the Indian Council of Philosophical Research Special Issue, XXVII(2), 2010.
W. van der Hoek and J.-J. Ch. Meyer. A complete epistemic logic for multiple agentsCcombining distributed and common knowledge. Epistemic Logic and the Theory of Games and Decisions, pages 35C68, 1997.
V. Vilasini, N. Nurgalieva, and L. del Rio. Multiagent paradoxes beyond quantum theory. New Journal of Physics, 21 (11), 2019.
Science Publishing Group
1 Rockefeller Plaza,
10th and 11th Floors,
New York, NY 10020
Tel: (001)347-983-5186