| Peer-Reviewed

Automated Proof Search System for Logic of Correlated Knowledge

Received: 4 October 2019     Accepted: 2 March 2020     Published: 14 April 2020
Views:       Downloads:
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.

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

Keywords

Logic of Correlated Knowledge, Sequent Calculus, Automated Proof System, Decidability, Soundness, Completeness, Admissibility of the Cut Rule

References
[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.
Cite This Article
  • 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

    Copy | Download

    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

    Copy | Download

    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

    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}
    }
    

    Copy | Download

  • 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  - 

    Copy | Download

Author Information
  • Institute of Computer Science, Vilnius University, Vilnius, Lithuania

  • Institute of Data Science and Digital Technologies, Vilnius University, Vilnius, Lithuania

  • Sections