逻辑学前沿报告向量空间、信念基础的逻辑 (2).pdf-淘文阁

资源描述

《逻辑学前沿报告向量空间、信念基础的逻辑 (2).pdf》由会员分享，可在线阅读，更多相关《逻辑学前沿报告向量空间、信念基础的逻辑 (2).pdf（62页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。

1、Rethinking Epistemic Logic with Belief Bases1Compact representation of epistemic attitudesEpistemic logic(EL):)Logical theory of epistemic attitudes(e.g.,belief,knowledge)Dynamic epistemic logic(DEL):)Logical theory of multi-agent epistemic dynamicsAI applications:Epistemic planningTheory of Mind(To

2、M)modelling for social robotsCryptographic protocolsBlockchainNeed for compact semantics2Universal epistemic modelIt contains all possible states of the world and all possible beliefhierarchiesWhy is it useful?Definition of maximal ignoranceModeling situations with no prior assumptions about agents

3、beliefsProbabilistic universal type space(Mertens&Zamir,1985)Qualitative version for epistemic logic S5n(Fagin et al.,1991)Both constructions are inductive and fairly complexAlternative construction:canonical modelIt requires a notion of consistency(and proof)Not exploitable in practice(e.g.,for mod

4、el checking),since it isinfinite3Universal epistemic model(cont.)Given an arbitrary set Y,let F(Y)be the set of functions with domain Yand codomain 0,1 and let Atm be the set of atomic facts.Inductive definition of belief hierarchies:States of the of world(0-order beliefs):Z0=F(Atm)Beliefs up to ord

5、er k+1:Zk+1=Zk F(Zk)nQualitative universal type space:Z0 F(Z0)n F(Z1)n.+an extra condition of coherence between dierent belief orders4Private belief changeModelling private belief change in DEL requires world“duplication”(Baltag et al.,1998;Gerbrandy&Groeneveld,1997)Nothing happensEpistemic modelCop

6、y 1Copy 2Private update for agent iAgent i updates her beliefsThe epistemic model grows exponentially5ProposalLogic of explicit and implicit belief with a semantics exploiting abelief base abstractionCompact representation of the universal epistemic model:No need for an inductive definitionIndepende

7、nt from proof theoryFinite representation(useful for model checking)“Parsimonious”account of private belief change:A private informative action modifies the belief base of a single agentNo need to“duplicate”modelsClarifying the connection between distributed belief and beliefmerging6Outline1A logic

8、of explicit and implicit belief2Universal epistemic model3Dynamic extensions4Recovering introspection5Explicit and implicit distributed belief7Outline1A logic of explicit and implicit belief2Universal epistemic model3Dynamic extensions4Recovering introspection5Explicit and implicit distributed belie

9、f8Possible worlds semantics vs.knowledge basesLogics of mental attitudes use extensional Kripke-style semantics:Epistemic logic(Fagin et al.,1995)Logic of preferences(van Benthem&Liu,2007)Logic of intention(Cohen&Levesque,1990)Knowledge base abstraction is widely used in AI and KR:Belief base(Makins

10、on,1985;Hansson,1993;Nebel,1992)Desire base(Benferhat et al.,2001),intention base(Shoham,2011)Modal base(Kratzer,1981)Belief baseB=1,nDesire baseD=1,mDecisionIntention base(agenda)I=1,kAction)How can the two approaches be reconciled?9Conceptual frameworkAgent1sbeliefbaseAgent2sbeliefbaseCommonground

11、Agent1simplicitbeliefsAgent2simplicitbeliefsDeduc9onDeduc9onCommon ground can be described as the“.presumedbackground information shared by participants in aconversation.”(Stalnaker,2002,p.701).10Logic of Doxastic Attitudes(LDA)Two primitive operators:Explicit belief 4iImplicit belief iNew semantics

12、 for epistemic logic:epistemic accessibility relationsare computed from belief bases11LanguageLanguage of Logic of Doxastic Attitudes(LDA):L0:=p|1 2|4iLLDA:=|1 2|ip ranges over infinite countable set Atm and i ranges over finite set Agt4i:agent i explicitly(actually)believes:is in agent is belief ba

13、sei:agent i implicitly(potentially)believes that Language of Epistemic Logic(EL):LEL:=p|1 2|iLEL LLDA12Multi-agent belief basesDefinition(Multi-agent belief base)A multi-agent belief base is a tuple B=(B1,.,Bn,V)where:Bi L0is agent is belief base,V Atm is the actual state.The set of multi-agent beli

14、ef bases is denoted by Univ.Definition(Satisfaction relation)Let B=(B1,.,Bn,V)be a multi-agent belief base.Then:B|=p()p 2 VB|=()B 6|=B|=1 2()B|=1and B|=2B|=4i()2 Bi13Epistemic accessibility relationDefinition(Epistemic alternatives)Let B=(B1,.,Bn,V),B0=(B01,.,B0n,V0)2 Univ.Then,BRiB0if and only if 8

15、 2 Bi:B0|=.14Multi-agent belief modelsDefinition(Multi-agent belief model)A multi-agent belief model(or simply model)is a pair(B,Cxt),where:B 2 Univ,andCxt Univ is the agents common ground(or context).The class of multi-agent belief models is denoted by M.Definition(Satisfaction relation(cont.)Let(B

17、correctness)(B,Cxt)satisfies belief correctness(BC)if and only if B 2 Cxt and,forevery B02 Cxt,B0RiB0.Proposition(B,Cxt)satisfies BC if and only ifB 2 Cxt and 8B02 Cxt,8i 2 Agt,8 2 B0i:B0|=.MXdenotes the model class satisfying all conditions in X GC,BC16AxiomaticsLogic LDA:Axioms of CPL(CPL)(i i(!)!

18、i(Ki)4i!i(Int4i,i),!(MP)i(Neci)Extra axioms:(i i)(Di)i!(Ti)Correspondence function:f(Di)=GCf(Ti)=BC17Axiomatics(cont.)TheoremLet X Di,Ti.Then,the logic LDAXis sound and complete forthe class Mf(x):x2X.18ComplexityPolynomial embedding of LDA into the logic of general awareness(Fagin&Halpern,1987),who

19、se satisfiability problem is known to bePSPACE-complete(Agotnes&Alechina,2014)Idea of the translation:Explicit belief (Implicit belief+Awareness)Implicit belief Implicit beliefTheorem(Complexity)Let X GC,BC.Then,checking satisfiability of formulas in LLDArelative to the class MXis a PSPACE-complete

20、problem.19Outline1A logic of explicit and implicit belief2Universal epistemic model3Dynamic extensions4Recovering introspection5Explicit and implicit distributed belief20Outline1A logic of explicit and implicit belief2Universal epistemic model3Dynamic extensions4Recovering introspection5Explicit and

21、 implicit distributed belief21-context and universal contextDefinition(-context)Let 2 L0.We defineUniv=B 2 Univ:B|=to be the-context.The universal context is Univ=Univ.Validity relative to universal context:|=Univ means that 8B 2 Univ:(B,Univ)|=22Models with maximal ignoranceDefinition(Model with ma

22、ximal ignorance)Let B=(B1,.,Bn,V)2 Univ such thatBi=;for every i 2 Agt.Then,(B,Univ)is called model with maximal ignorance.PropositionLet(B,Univ)be a model with maximal ignorance.Then,is satisfiable for the class M if and only if(B,Univ)|=i.23Model checking problem-context model checkingGiven:2 LLDA

23、,2 L0and finite B 2 Univ.Question:Do we have(B,Univ)|=?TheoremThe-context model checking problem is PSPACE-complete.Proof idea.Hardness:polynomial reduction of TQBF.Membership:adaptation of PSPACE-complete tableau-based satisfiabilitychecking procedure to model checking.Consequence:-context model ch

24、ecking has the same complexity assatisfiability checking24Kripke semantics for epistemic logic languageDefinition(Kripke structure)A Kripke structure is a tuple K=(S,)1,.,)n,!)such that:S is a set of states,)i S S is agent is epistemic accessibility relation,!:Atm?!2Sis a valuation function.A pointe

25、d Kripke structure is a pair(K,s)with s 2 S.Interpretation of language LEL:(K,s)|=p()s 2!(p)(K,s)|=()(K,s)6|=(K,s)|=()(K,s)|=and(K,s)|=(K,s)|=i()8s02 S:if s)is0then(K,s0)|=K:class of Kripke strucutresPK:class of pointed Kripke structures25Equivalence resultTheoremLet 2 LEL.Then,the following three s

26、tatements are equivalent:|=M,|=K,|=Univ.26Language of extended epistemic logicLEEL:=p|1 2|i|riri:agent i believes at most that(B,Cxt)|=ri()8B02?Cxt Ri(B)?:(B0,Cxt)|=where Ri(B)=B0:BRiB027Only believing and universal modalityUdef=i riOidef=i riU:is universally trueOi:all that agent i believes is 28(N

27、on)equivalence resultsPropositionWe have the following relationship between sets of validities:2 LEEL:|=M 2 LEEL:|=Univ.Example of formula?such that 6|=M?and|=Univ?:?def=E?p2Xp q2Yq?withE def=U and finite,non-empty X,Y Atm such that X Y=;TheoremLet 2 LEEL.Then,|=M if and only if|=K.29Equivalence wit

28、h qualitative universal type space semanticsInductive definition of the qualitative version of universal type spacefor systems Knand KTn)Adapted from construction for S5nby Fagin et al.(1991)Result:equivalence between universal context and qualitativeuniversal type space semantics relative to the la

29、nguage LEEL30Outline1A logic of explicit and implicit belief2Universal epistemic model3Dynamic extensions4Recovering introspection5Explicit and implicit distributed belief31Outline1A logic of explicit and implicit belief2Universal epistemic model3Dynamic extensions4Recovering introspection5Explicit

30、and implicit distributed belief32Multi-agent belief dynamicsPublic information)common ground changePrivate information)belief base change:Belief base expansionForgettingBelief base revision.33Extension by public announcements!:holds after the public announcement of(B,Cxt)|=!()if(B,Cxt)|=then(B,Cxt!)

31、|=where:Cxt!=B02 Cxt:(B0,Cxt)|=)It works for classes M and MBC)It does not work for class MGC34Reduction axioms|=M!p$(!p)|=M!$(!)|=M!(1 2)$(!1!2)|=M!4i$4i|=M!i$(!i!)35Extension by private belief base expansion+i:holds after agent i 2 Agt has privately expanded her beliefbase by(B,Cxt)|=+i()(B+i,Cxt)

33、d by private belief baseexpansion operators is PSPACE-complete.37Extension by private forgetting?i:holds after agent i 2 Agt has privately forgotten(B,Cxt)|=?i()(B?i,Cxt)|=with B?i=(B?i1,.,B?in,V)and:B?ii=Bi B?ij=Bjif i 6=j)It works for both classes M and MGC)It does not work for class MBC38Comparis

34、on with DELDefinition(Model transformation)Model transformation is the functiontransf:M?!PKsuch that transf?(B,Cxt)?=(K,s)if and only if:S=?sB0:B02 B Cxt,for every i 2 Agt,)i=?(sB0,sB00)2 S S:B02 Cxt B,B002 Cxt and B0RiB00,for every p 2 Atm,!(p)=sB02 S:p 2 V0,ands=sB.“Tracking information”functor in

35、 the sense of(van Benthem,2016)8 2 LEL:(B,Cxt)|=i transf?(B,Cxt)?|=39Comparison with DEL(cont.)Definition(Private update of a pointed Kripke structure)Let K=(S,)1,.,)n,!)and s 2 S.The private update of(K,s)by for i,denoted by(K,s)(i,),is the pair(K0,s1)such that:S0=s01:s02 S s02:s02 S,for all s02 S

36、and for all j 2 Agt:)0j(s01)=?s002:s0)js00and(M,s00)|=if i=j,)0j(s01)=?s002:s0)js00 if i 6=j,)0j(s02)=?s002:s0)js00,and for all p 2 Atm:!0(p)=s012 S0:s02!(p)s022 S0:s02!(p).Special case of arrow-elimination update(Kooi&Renne,2011)40Comparison with DEL(cont.)8j 2 Agt8j 2 Agt?Kripke structureCopy 1Cop

37、y 2j 6=ii?(i,?)41Comparison with DEL(cont.)TheoremThe pointed Kripke structure transf?(B+i,Cxt)?and the pointedKripke structure transf?(B,Cxt)?(i,)are bisimilar.42Comparison with DEL(cont.)Private belief base expansion(B,Cxt)(K,s)(B+i,Cxt)(K,s)(i,)(K?,s?)transftransfbisimilarPrivate update43Comparis

38、on with DEL(cont.)Let i0,.,im2 Agt and 0,.,m2 L0.Moreover,let(B0,Cxt)2 M and(K0,s0)2 PK such thattransf?(B0,Cxt)?=(K0,s0).For every 1 k m:(Bk,Cxt)=(B+ik?1k?1k?1,Cxt),(Kk,sk)=(Kk?1,sk?1)(ik?1,k?1).Then,|Sm|=|S0|2mwhile|Bm|B0|+m.The size of the original Kripke structure increases exponentially in thel

39、ength of the sequence of private update operations!The size of the original model increases at most linearly in the length ofthe sequence of private belief base expansion operations!44Outline1A logic of explicit and implicit belief2Universal epistemic model3Dynamic extensions4Recovering introspectio

40、n5Explicit and implicit distributed belief45Outline1A logic of explicit and implicit belief2Universal epistemic model3Dynamic extensions4Recovering introspection5Explicit and implicit distributed belief46Recovering introspectionPrivate belief base expansion does not necessarily preserve positiveintr

41、ospection closure on implicit beliefsPropositionThere exists(B,Cxt)2 M such that:8 2 LLDA,8i 2 Agt:(B,Cxt)|=i!ii,9i 2 Agt,9 2 L0,9 2 LLDA:(B+i,Cxt)|=i and(B+i,Cxt)|=ii.The same for negative introspection47Recovering introspection(cont.)Definition(Epistemic alternatives for introspectively discerning

44、(Atm,Agt)and G ranges over 2Agt=2Agt;G:coalition G implicitly(potentially)believes that 52SemanticsDefinition(Pooling)Let B=(B1,.,Bn,V)2 Univ and let G 2 2Agt.ThenPoolG(B)=i2GBi.Definition(Collective epistemic alternatives)Let G 2 2Agtand B=(B1,.,Bn,V),B0=(B01,.,B0n,V0)2 Univ.Then,BRGB0if and only i

45、f 8 2 PoolG(B):B0|=.53Semantics(cont.)Definition(Satisfaction relation(cont.)Let(B,Cxt)be a MAB.Then:(B,Cxt)|=G()8B02 Cxt:if BRGB0then(B0,Cxt)|=54AxiomaticsAxioms of CPL(CPL)(i i(!)!i(Ki)4i!i(Int4i,i)G!G0 if G G0(MonG),!(MP)i(Neci)55Recovering consistencyDefinition(Maximally consistent subsets of co

47、B)X.Definition(Doxastic alternatives for doxastically consistent(dc)coalitions)Let G 2 2Agtand B=(B1,.,Bn,V),B0=(B01,.,B0n,V0)2 Univ.Then,BRdcGB0if and only if 8 2 CombG(B):B0|=.57Recovering consistency(cont.)(B,Cxt)|=dcG()8B02 Cxt:if BRdcGB0then(B0,Cxt)|=PropositionLet G 2 2Agtand B 2 Univ.Then,(B,

48、Univ)|=dcG,where dcGdef=dcG.TheoremThe-context model checking problems for the extensions of LLDAbyimplicit distributed belief(G)and doxastically consistent implicitdistributed belief(dcG)remain PSPACE-complete.58Hidden track:graded belief:=|1 2|kiwhere ranges over L0,i ranges over Agt and k ranges

49、over Nki:agent i would believe that,if she removed k pieces of information from her belief base:agent i implicitly believes that with strength k59Hidden track:graded belief(cont.)Definition(Graded doxastic alternatives)Let i 2 Agt,k 2 N andB=(B1,.,Bn,V),B0=(B01,.,B0n,V0)2 Univ:BRkiB0if and only if|S

50、at(B0,Bi)|?|Bi|?k?,where Sat(B0,Bi)=2 Bi:B0|=.(B,Cxt)|=ki()8B02 Cxt:if BRkiB0then(B0,Cxt)|=60AxiomaticsAxioms and rules of inference of LDA plus:ki!ik0 if k0 k?2X4i?!ki?_X0X:|X0|?|X|?k?2X0?if|X|k61Thank you for your attention!For more details:E.Lorini(2020).Rethinking Epistemic Logic with Belief Bas

展开阅读全文