# Automated proof search system for logic of correlated knowledge

## TL;DR

This paper introduces an automated proof search system for the logic of correlated knowledge, demonstrating its soundness, completeness, and decidability through a sequent calculus framework.

## Contribution

It presents a novel automated proof search system with a sequent calculus for the logic of correlated knowledge, establishing its decidability and key proof properties.

## Key findings

- Proof search terminates successfully for the logic of correlated knowledge
- The system is sound and complete with respect to the logic
- Decidability of the logic is achieved through the proof system

## Abstract

The automated proof search system and decidability for logic of correlated knowledge is presented in this paper. The core of the proof system is the sequent calculus with the properties of soundness, completeness, admissibility of cut and structural rules, and invertibility of all rules. The proof search procedure based on the sequent calculus performs automated terminating proof search and allows us to achieve decision result for logic of correlated knowledge.