公开宣告逻辑的一个加标矢列演算.pdf
《公开宣告逻辑的一个加标矢列演算.pdf》由会员分享,可在线阅读,更多相关《公开宣告逻辑的一个加标矢列演算.pdf(19页珍藏版)》请在咨信网上搜索。
1、Studies in Logic,Vol.16,No.3(2023):89107PII:16743202(2023)03008919A Labelled Sequent Calculus for PublicAnnouncement LogicHao WuHans van DitmarschJinsheng ChenAbstract.Public announcement logic(PAL)is an extension of epistemic logic(EL)withsome reduction axioms.In this paper,we propose a cutfree lab
2、elled sequent calculus for PAL,which isan extension of that forEL with sequentrules adapted fromthe reductionaxioms.Thiscalculus admits cut and allows terminating proof search.1IntroductionThe modern modal approach to the logic of knowledge and belief was extensively developed by Hintikka(10)to inte
3、rpret epistemic notions utilizing possibleworld semantics.The standard multiagent epistemic logic EL is usually identifiedwiththepolymodalmodallogicS5foragroupofagents.Publicannouncementlogic(PAL),introduced by Plaza(17),is an extension of EL that studies logical dynamics of epistemic information af
4、ter the action of public announcement.More generalactions are studied in action model logic(see e.g.4,5,7).PALisanextensionofELwithannouncementoperatorsoftheform.AsEL,formulas in PAL are interpreted in Kripke models in which all relations are reflexive,transitive and symmetric.In particular,formulas
5、 of the form are interpreted inthe restrictions of Kripke models induced by the announcement.The Hilbertstyleaxiomatization of PAL is obtained by adding to that of EL the so called reductionaxioms for announcement operators,which can be used to eliminate announcementoperators in a PALformula.General
6、ly speaking,it is difficult to prove whether proof search using a Hilbertstyle axiomatization is decidable.In view of these,many proof systems for PALare proposed in the literature,e.g.,tableau systems(3),labelled sequent calculi(2,16).Received 20220718Revision Received 20221104Hao WuInstitute of Lo
7、gic and Cognition,Sun Yatsen UniversityDepartment of Philosophy,Sun Yatsen UHans van DitmarschCNRS,University of Toulouse,IRIThans.vanditmarschloria.frJinsheng ChenDepartment of Philosophy(Zhuhai),Sun Yatsen U90Studies in Logic,Vol.16,No.3(2023)In this paper,we propose another labelled sequent calcu
8、lus for PAL.This calculus is based on a labelled sequent calculus for EL proposed by Hakli and Negri(9)and rules for announcement operators designed according to the reduction axioms.This calculus admits structural rules(including cut)and allows terminatingproof search.Unlike 2,16,which are based on
9、 another semantics for PAL,ourcalculus is based on the original semantics and takes into account the conditions ofreflexivity,transitivity and symmetry in EL.The rest of the paper is structured as follows:Section 2 presents some basicnotions and concepts.Section 3 presents our labelled sequent calcu
10、lus GPALforPAL.Section4showsthatGPALadmitssomestructuralrules,includingcut.Section5 shows that GPALallows terminating proof search.Section 6 compares GPALwithrelated works,concludes the paper and discusses future work.2Preliminaries2.1EL and PALLet Prop be a denumerable set of variables and Ag a fin
11、ite set of agents.Language LELfor epistemic logic is defined inductively as follows:L :=p|KaMoreover,language LPALfor public announcement logic is defined inductively asfollows:L :=p|Ka|where p Prop and a Ag.We use as an abbreviation for()().LPALis an extension of LELwith announcement formulas.An ep
12、istemic frame F is a tuple(W,aaAg),where W is a set of states anda W W is a reflexive,transitive and symmetric relation for each a Ag.An epistemic model M is a tuple(W,aaAg,V)where(W,aaAg)isan epistemic frame and V is a function from Prop to P(W).Let M=(W,aaAg,V)be an epistemic model and w W.The not
13、ion of being true at w in M(notation:M,w )is defined inductively as follows:M,w piffw V(p)M,w iffM,w M,w iffM,w and M,w M,w iffM,w or M,w M,w Kaifffor all v W,w av implies M,v M,w iffM,w implies M,w where M=(W,aaAg,V)is the model restricted to with W=w W|M,w ,a=a(W W)and V=V(p)W.Hao Wu,Hans van Ditm
14、arsch,Jinsheng Chen/A Labelled Sequent Calculus for Public Announcement Logic91A formula is globally true in an epistemic model(notation:M )ifM,w for all w W.A formula is valid in an epistemic frame F if F,V for all valuations V.Epistemic logic EL is the set of LELformulas that are valid on the clas
15、s of allepistemic frames.Public announcement logic PAL is the set of LPALformulas thatare valid on the class of all epistemic frames.EL is axiomatized by(Tau),(K),(4),(T),(5),(MP)and(GKa).PAL is axiomatized by the axiomatization for EL plus reduction axioms(R1)(R6):(Tau)Classical propositional tauto
16、logies.(K)Ka()(Ka Ka)(4)Ka KaKa(T)Ka (5)Ka KaKa(MP)From and infer.(GKa)From infer Ka.(R1)p (p)(R2)()(R3)()()(R4)()()(R5)Ka (Ka)(R6)Remark 1.The standard language for PAL does not contain.To simplify ourwriting,we add to our language.Because of its existence,(R4)is added to theaxiomatization.2.2Label
17、led sequent calculusA labelled sequent calculus for a logic with Kripke semantics is based on theinternalization of Kripke semantics.Let F=(W,aaAg)be an epistemic frame.A relational atom is of theform x ay,where x,y W and a Ag.A labelled formula is of the form x:,where x W and is an LELformula.We us
18、e,with or without subscript todenote relational atoms or labelled formulas.A multiset is a set with multiplicity,or put the other way round,a sequencemodulo the ordering.A labelled sequent is of the form where,are finitemultisets of relational atoms and labelled formulas.A sequent rule is of the for
19、m(R)1 1.m m where m 0.1 1,.,m mare called premises of this rule and is called the conclusion.If m=0,we simply write and call it an initialsequent.The formula with the connective in a rule is the principal formula of thatrule,and its components in the premisses are the active formulas.A labelled sequ
20、entcalculus is a set of sequent rules.A derivation in a labelled sequent calculus G isdefined as usual.The derivation height h of a sequent is defined as the length of92Studies in Logic,Vol.16,No.3(2023)longest branch in the derivation of the sequent.We use G to denote that is derivable in G and G h
21、 to denote that is derivable in Gwith a derivation of height which is at most h.A sequent rule(R)is admissible in G if G i ifor 1 i m impliesG .It is heightpreserving admissible if G hi ifor 1 i mimplies G h .Let M=(W,aaAg,V)be an epistemic model.The interpretation Mofrelational atoms and labelled f
22、ormulas are defined as follows:M(x ay)=x ay;M(x:)=M,x .A labelled sequent 1,.,m 1,.,nis valid ifMx1xkM(1)M(m)M(1)M(n)is true,where M=(W,aaAg,V)is an epistemic model,and x1,.,xkarevariables occurring in 1,.,m 1,.,nranging over W.A sequent rule R is valid if the validity of all the premises implies th
23、e validityof the conclusion.GivenalabelledsequentcalculusGandalogic,wesayGisalabelledsequentcalculus for if for all,G if and only if .2.3Labelled sequent calculus for ELDefinition1.LabelledsequentcalculusGELforELconsistsofthefollowinginitialsequents and rules1:(1)Initial sequents:x:p,x:px ay,x ay(2)
24、Propositional rules:(),x:x:,()x:,x:()x:1,x:2,x:1 2,(),x:1 ,x:2 ,x:1 2(),x:x:,x:,()x:,x:,x:1It is mentioned without proof in 9 that this is a labelled sequent calculus for EL.This calculus isa multiagent version of the labelled sequent calculus for S5 proposed in 14.Hao Wu,Hans van Ditmarsch,Jinsheng
25、 Chen/A Labelled Sequent Calculus for Public Announcement Logic93(3)Modal rules:(Ka)y:,x:Ka,x ay,x:Ka,x ay,(Ka)x ay,y:,x:Kawhere y does not occur in the conclusion of(Ka).(4)Relational rules:(Refa)x ax,(Transa)x az,x ay,y az,x ay,y az,(Syma)y ax,x ay,x ay,Proposition 1.For any LELformula,GEL x:,x:.P
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 公开 宣告 逻辑 一个 加标矢列 演算
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。