A Sequent Calculus For Public Announcement Logic Based On Context-dependent Semantics

Public Announcement Logic was widely applied to reason about knowledge changes under public communications.However,the knowledge changes and reasoning under public communications are rather complicated.Although the semantics of PAL has shown its power to represent the knowledge change caused by announcements,facing the knowledge reasoning,a deduction system that can easier handle the proof of theorems than axiomatic system is needed.A possible approach is the sequent calculus for PAL.In this thesis,I constructed a sequent calculus,G3 PALC,for Public Announcement Logic based on Context-dependent Semantics.I showed that those theorems that cannot be proved in G3 PAL can be proved in G3 PALC and those rules for composition axiom are no longer necessary in G3 PALC.Moreover,when compared with GPAL,there is no need to add relational rules to G3 PALC and composition axioms can be proved without other lemmas.G3-style is also inherited by G3 PALC which means weakening rules and contraction rules are admissible.Finally,I proved the equivalence between G3 PALC,HPAL and GPAL and the equivalence between world-deletion semantics,link-cutting semantics and context-dependent semantics.Chapter 1 introduces our research theme,research background and some relevant works.Chapter 2 is the preliminary of this thesis involving the standard semantics and Hilbert-style axiomatization of PAL and the methodology used in proving completeness in HPAL.Chapter 3 reviews the existing sequent calculus for Public Announcement Logic G3 PAL and GPAL.Chapter 4 provides the sequent calculus G3 PALC based on Context-dependent Semantics,a proof of completeness for G3 PALC,the equivalence between G3 PALC,G3PAL and GPAL as well as the equivalence between World-deletion semantics,Link-cutting semantics and context-dependent semantics.