| Title |
Cut-free sequent calculus for multi-agent logic of common knowledge |
| Authors |
Alonderis, Romas ; Giedra, Haroldas |
| DOI |
10.37256/cm.6220255621 |
| Full Text |
|
| Is Part of |
Contemporary mathematics.. Singapore : Universal Wiser Publisher. 2025, vol. 6, iss. 2, p. 1988-2003.. ISSN 2705-1064. eISSN 2705-1056 |
| Keywords [eng] |
common knowledge ; sequent calculus ; loops, decidability |
| Abstract [eng] |
Cut-free sequent calculi are handy tools for backward proof-search of logical formulas or sequents. In the present paper, we introduce a Gentzen-type sequent calculus for the logic of common knowledge. To maintain a deterministic backward proof-search process, we do not include cut or cut-like rules in the introduced calculus. Also, derivation loops are used to define provable sequents and to establish termination of backward proof-search. Using this sound and complete finitary loop-type sequent calculus we construct a decision procedure for the logic of common knowledge. The procedure allows to efficiently determine whether an arbitrary formula or sequent is valid in the logic. |
| Published |
Singapore : Universal Wiser Publisher |
| Type |
Journal article |
| Language |
English |
| Publication date |
2025 |
| CC license |
|
