A Labelled Sequent Calculus for Public Announcement Logic

TL;DR

This paper introduces a cut-free labelled sequent calculus for Public Announcement Logic (PAL), enabling efficient proof search and extending the existing calculus for epistemic logic with rules based on reduction axioms.

Contribution

It presents the first cut-free labelled sequent calculus for PAL, incorporating rules from reduction axioms to facilitate proof search.

Findings

The calculus admits cut and allows terminating proof search.

It extends the calculus for epistemic logic with new sequent rules.

Provides a foundation for automated reasoning in PAL.

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.