A Labelled Sequent Calculus for Public Announcement Logic

2022/07/21 by Wu, Hao, van Ditmarsch, Hans, Chen, Jinsheng · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2207.10262

Abstract

Public announcement logic(PAL) is an extension of epistemic logic (EL) with some reduction axioms. In this paper, we propose a cut-free labelled sequent calculus for PAL, which is an extension of that for EL with sequent rules adapted from the reduction axioms. This calculus admits cut and allows terminating proof search.

Cited by

• Dynamic Hypersequents for Public Announcement Logic

Related

• Dynamic Hypersequents for Public Announcement Logic
• A Sequent Calculus and a Theorem Prover for Standard Conditional Logics
• Public Announcement Logic in HOL
• Sequent Calculus for Intuitionistic Epistemic Logic
• Proof search for propositional abstract separation logics via labelled sequents