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.
| Published in | American Journal of Mathematical and Computer Modelling (Volume 5, Issue 2) |
| DOI | 10.11648/j.ajmcm.20200502.11 |
| Page(s) | 29-42 |
| Creative Commons |
This is an Open Access article, distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution and reproduction in any medium or format, provided the original work is properly cited. |
| Copyright |
Copyright © The Author(s), 2020. Published by Science Publishing Group |
Logic of Correlated Knowledge, Sequent Calculus, Automated Proof System, Decidability, Soundness, Completeness, Admissibility of the Cut Rule
| [1] | D. Aerts. Description of compound physical systems and logical interaction of physical systems. Current Issues on Quantum Logic, 8: 381C405, 1981. |
| [2] | A. Araujo and M. Finger. A formal system for quantum communication environments. VIII - Brazilian National Meeting for Artificial Intelligence, pages 1C11, 2011. |
| [3] | A. Baltag and S. Smets. Correlated knowledge: an epistemic-logic view on quantum entanglement. International Journal of Theoretical Physics, 49 (12): 3005C3021, 2010. |
| [4] | A. Baltag and S. Smets. Logics of informational interactions. Journal of Philosophical Logic, 44: 595C 607, 2015. |
| [5] | A. Baltag and S. Smets. Modeling correlated information change: from conditional beliefs to quantum conditionals. Soft computing, 21 (6): 1523C1535, 2017. |
| [6] | G. Battilotti. Characterization of quantum states in predicative logic. Int. J. Theor. Phys., 50: 3669C3681, 2011. |
| [7] | G. Birkhoff and J. von Neumann. The logic of quantum mechanics. Annals of Mathematics, 37: 823C843, 1936. |
| [8] | F. Boge. Quantum information vs. epistemic logic: An analysis of the frauchiger-renner theorem. Foundations of Physics, 49 (10): 1143C1165, 2019. |
| [9] | B. Coecke, C. Heunen, and A. Kissinger. Compositional quantum logic. Computation, Logic, Games, and Quantum Foundations, pages 21C36, 2013. |
| [10] | 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. |
| [11] | G.Gentzen. Untersuchungenuberdaslogischeschliesen. i. Mathematische Zeitschrift, 39 (2): 176C210, 1934. |
| [12] | S. Kripke. Semantical analysis of modal logic i. normal propositional calculi. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 9: 67C96, 1963. |
| [13] | G. Mackey. Quantum mechanics and hilbert space. American Mathematical Monthly, 64 (2): 45C57, 1957. |
| [14] | G. Mackey. The mathematical foundations of quantum mechanics. W.A. Benjamin, NY, 1963. |
| [15] | S. Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34 (5): 507C544, 2005. |
| [16] | S. Negri and J. von Plato. Structural Proof Theory. Cambridge University Press, 2001. |
| [17] | N. Nurgalieva and L. del Rio. Inadequacy of modal logic in quantum settings. EPTCS 287, pages 267C297, 2019. |
| [18] | C. Piron. Foundations of quantum physics. W.A. Benjamin Inc., Massachusetts, 1976. |
| [19] | C. Randall and D. Foulis. Tensor products of quantum logics do not exist. Notices Amer. Math. Soc., 26 (6), 1979. |
| [20] | S. Smets. Logic and quantum physics. Journal of the Indian Council of Philosophical Research Special Issue, XXVII(2), 2010. |
| [21] | 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. |
| [22] | V. Vilasini, N. Nurgalieva, and L. del Rio. Multiagent paradoxes beyond quantum theory. New Journal of Physics, 21 (11), 2019. |
APA Style
Haroldas Giedra, Romas Alonderis. (2020). Automated Proof Search System for Logic of Correlated Knowledge. American Journal of Mathematical and Computer Modelling, 5(2), 29-42. https://doi.org/10.11648/j.ajmcm.20200502.11
ACS Style
Haroldas Giedra; Romas Alonderis. Automated Proof Search System for Logic of Correlated Knowledge. Am. J. Math. Comput. Model. 2020, 5(2), 29-42. doi: 10.11648/j.ajmcm.20200502.11
AMA Style
Haroldas Giedra, Romas Alonderis. Automated Proof Search System for Logic of Correlated Knowledge. Am J Math Comput Model. 2020;5(2):29-42. doi: 10.11648/j.ajmcm.20200502.11
Share This Article
Twitter
Linked In
Facebook
Copy
Download@article{10.11648/j.ajmcm.20200502.11,
author = {Haroldas Giedra and Romas Alonderis},
title = {Automated Proof Search System for Logic of Correlated Knowledge},
journal = {American Journal of Mathematical and Computer Modelling},
volume = {5},
number = {2},
pages = {29-42},
doi = {10.11648/j.ajmcm.20200502.11},
url = {https://doi.org/10.11648/j.ajmcm.20200502.11},
eprint = {https://article.sciencepublishinggroup.com/pdf/10.11648.j.ajmcm.20200502.11},
abstract = {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.},
year = {2020}
}
TY - JOUR T1 - Automated Proof Search System for Logic of Correlated Knowledge AU - Haroldas Giedra AU - Romas Alonderis Y1 - 2020/04/14 PY - 2020 N1 - https://doi.org/10.11648/j.ajmcm.20200502.11 DO - 10.11648/j.ajmcm.20200502.11 T2 - American Journal of Mathematical and Computer Modelling JF - American Journal of Mathematical and Computer Modelling JO - American Journal of Mathematical and Computer Modelling SP - 29 EP - 42 PB - Science Publishing Group SN - 2578-8280 UR - https://doi.org/10.11648/j.ajmcm.20200502.11 AB - 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. VL - 5 IS - 2 ER -
Information
Email: