逻辑学前沿报告向量空间、信念基础的逻辑 (4).pdf

《逻辑学前沿报告向量空间、信念基础的逻辑 (4).pdf》由会员分享，可在线阅读，更多相关《逻辑学前沿报告向量空间、信念基础的逻辑 (4).pdf（139页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、Reasoning and Completeness inHybrid LogicTodays goalsIn todays talk I first want to introduce hybrid logic,a form of modallogic in which it is possible to name worlds(or times,or computationalstates,or situations,.or indeed,whatever it is that the elements ofKripke Models are taken to represent).I t

2、hen want to:Discuss a basic reasoning pattern in hybrid logic;andDiscuss some themes in hybrid completeness theory.At the end I will point to other reasoning styles for hybrid logic(such asnatural deduction)and to recent work on formalizing completeness proofsfor hybrid logic.I wont have time to giv

3、e many details here,but I willgive lots of pointers to this literature.But also:a little history.For hybrid logic,history starts withArthur Prior(1949 1969).Prior isbest known as the inventor of tenselogic,the logic of future and past,which evolved into the varioustemporal logics used in moderncompu

4、ter science,and some of youmay also have come across famouspapers like The Runabout InferenceTicket or Thank Goodness thats over.But he also invented hybrid logic something that was long overlooked.What is modal logic?Slogan 1:Modal languages are simple yet expressive languages fortalking about rela

5、tional structures.Slogan 2:Modal languages provide an internal,local perspectiveon relational structures.Slogan 3:Modal languages are not isolated formal systems.These slogans pretty much sum up the Amsterdam perspectiveon modal logic.Slogans from:Preface to Modal Logic,by Blackburn,de Rijke and Ven

6、ema,Cambridge University Press,2001Propositional Modal LogicGiven propositional symbols PROP=p,q,r,.,and modality symbolsMOD=m,m0,m00,.the basic modal language(over PROP andMOD)is defined as follows:WFF:=|p|hmi|mIf theres just one modality symbol in the language,we usually write 3and 2 for its diamo

7、nd and box forms.Classic interpretation:3 means is possible;2 means is necessary,Boxes and diamonds are interdefinable:2 can be regarded as shorthandfor 3.And 3 can be regarded as shorthand for 2.Kripke ModelsA Kripke model M is a triple(W,R,V),where:W is a non-empty set,whose elements can be though

8、t ofpossible worlds,or epistemic states,or times,or states in atransition system,or geometrical points,or people standing invarious relationships,or nodes in a parse tree indeed,prettymuch anything you like.R is a collection of binary relation on W(one for eachmodality)V is a valuation assigning sub

9、sets of W to propositionalsymbols.The component(W,R)traditionally call a frame.Satisfaction DefinitionM,w?piffw V(p),where p PROPM,w?iffM,w 6?M,w?iffM,w?and M,w?M,w?iffM,w?or M,w?M,w?iffM,w 6?or M,w?M,w?hmiiffw0(wRmw0&M,w0?)M,w?miffw0(wRmw0 M,w0?).Note the internal perspective:we evaluate formulas i

10、nside mod-els,at particular states.Modal formulas are like little creaturesthat explore models by moving between related points.This isa key modal intuition,gives rise to the notion of bisimulation,and is the driving force for at least one traditional application.Tense logichfi means“at some Future

11、state”hpi means“at some Past state”.hpimia unconscious is true iffwecan look back in time from the currentstate and see a state where Mia isunconscious.Works a bit like thesentence Mia has been unconscious.hfimia unconscious requires us toscan the states that lie in the futurelooking for one where M

12、ia isunconscious.Works a bit like thesentence Mia will be unconscious.Description logicAnd,moving into the heart of ordinary extensional logic,considerdescription form a logical language computer scientists call ALC:killer u employer.gangsterThis means exactly the same thing as the modal formula:kil

13、ler hemployerigangsterDescription logicAnd,moving into the heart of ordinary extensional logic,considerdescription form a logical language computer scientists call ALC:killer u employer.gangsterThis means exactly the same thing as the modal formula:killer hemployerigangsterBut theres lots of other w

14、ays of talking about graphsTheres nothing magic about frames or Kripke models.Frames(W,R),are just a directed multigraphs(or labelledtransition systems).Valuations simply decorate states with properties.So a Kripke model for the basic modal language are just(verysimple)relational structures in the u

15、sual sense of first-order modeltheory.So we dont have to talk about Kripke models using modal logic we could use first-order logic,or second-order logic,or infinitarylogic,or fix-point logic,or indeed any logic interpreted overrelational structures.(The Johan van Benthem message!)Lets see how we can

16、 re-express the formulas we saw earlier in firstorder logic.Doing it first-order style(I)Consider the modal representationhfimia unconsciouswe could use instead the first-order representationt(tot MIA UNCONSCIOUS(t).Doing it first-order style(I)Consider the modal representationhfimia unconsciouswe c

17、ould use instead the first-order representationt(to|hmi|m|iSemanticsAs before,a model M is a triple(W,R,V).As before,(W,R)is just a frame(a labelled transitionsystem).The difference lies in V.Now a valuation V is a function withdomain PROPNOM and range Pow(W)such that for alli NOM,V(i)is a singleton

18、 subset of W.That is,a valuation makes each nominal true at a uniquestate;the nominal labels this state by being true there andnowhere else.We call the unique state w that belongs to V(i)thedenotation of i under V.Satisfaction DefinitionM,w?aiffw V(a),where a PROP NOMM,w?iffM,w 6?M,w?iffM,w?and M,w?

19、M,w?iffM,w?or M,w?M,w?iffM,w 6?or M,w?M,w?hmiiffw0(wRmw0&M,w0?)M,w?miffw0(wRmw0 M,w0?).M,w?iiffM,i?,where i is thedenotation of i under V.Tense logicOn the road to capturing AI temporal representationformalisms such as Allens logic of temporal reference:i isclearly doing the same sort of job as some

20、thing likeHolds(e,i).And we can now handle natural language examples moreconvincingly.Lets go back to the Vincent example.Tense in textVincent woke up.Something felt very wrong.Vincent reachedunder his pillow for his gun.P(i vincent-wake-up)P(j something-feel-very-wrong)jiP(k vincent-reach-under-pil

21、low-for-gun)kPiThis is not just a linguistic example!Note that ji is an equality,and is a formula expressing how kPi how two times are related.Tense in textVincent woke up.Something felt very wrong.Vincent reachedunder his pillow for his gun.P(i vincent-wake-up)P(j something-feel-very-wrong)jiP(k vi

22、ncent-reach-under-pillow-for-gun)kPiThis is not just a linguistic example!Note that ji is an equality,and is a formula expressing how kPi how two times are related.Tense in textVincent woke up.Something felt very wrong.Vincent reachedunder his pillow for his gun.P(i vincent-wake-up)P(j something-fee

23、l-very-wrong)jiP(k vincent-reach-under-pillow-for-gun)kPiThis is not just a linguistic example!Note that ji is an equality,and is a formula expressing how kPi how two times are related.Tense in textVincent woke up.Something felt very wrong.Vincent reachedunder his pillow for his gun.P(i vincent-wake

24、-up)P(j something-feel-very-wrong)jiP(k vincent-reach-under-pillow-for-gun)kPiThis is not just a linguistic example!Note that ji is an equality,and is a formula expressing how kPi how two times are related.Tense in textVincent woke up.Something felt very wrong.Vincent reachedunder his pillow for his

25、 gun.P(i vincent-wake-up)P(j something-feel-very-wrong)jiP(k vincent-reach-under-pillow-for-gun)kPiThis is not just a linguistic example!Note that ji is an equality,and is a formula expressing how kPi how two times are related.Tense in textVincent woke up.Something felt very wrong.Vincent reachedund

26、er his pillow for his gun.P(i vincent-wake-up)P(j something-feel-very-wrong)jiP(k vincent-reach-under-pillow-for-gun)kPiThis is not just a linguistic example!Note that ji is an equality,and is a formula expressing how kPi how two times are related.Description logic(I)We can now make ABox statements.

27、For example,to capture theeffect of the(conceptual)ABox assertionmia:Beautifulwe can writemiaBeautifulBasic hybrid language clearly modalNeither syntactical nor computational simplicity,nor general styleof modal logic,has been compromised.Nominals just atomic formulas.Satisfaction operators follow t

28、he normality rules/axioms.Theyare normal modal operators,just like 2:i()(i i)is valid.If is valid,then so is i.Indeed,satisfaction operators are even self-dual modaloperators:i and i say exactly the same thing.Basic hybrid logic is computableEnriching ordinary propositional modal logic with both nom

29、inalsand satisfaction operators does not effect computability.The basichybrid logic is decidable.Indeed we even have:Theorem:The satisfiability problem for basic hybrid languagesover arbitrary models is pspace-complete.1That is(up to a polynomial)the hybridized language has the samecomplexity as the

30、 orthodox modal language we started with.1Theorem 1 in“A roadmap of the complexity of hybrid logics”,CarlosAreces,Patrick Blackburn,and Maarten Marx,Computer science logic(J.Flumand M.Rodriguez-Artalejo,editors),LNCS,no.1683,Springer,1999,Proceedings of the 8th Annual Conference of the EACSL,Madrid,

31、September1999,pp.307-321.Standard TranslationAny basic hybrid formula can by converted into an equi-satisfiablefirst-order formula.All we have to do is add a first-order constant(orvariable)i for each nominal i and translate as follows(note the use ofequality):stx(p)=Pxstx(i)=(i=x)stx()=stx()stx()=s

32、tx()stx()stx(hRi)=y(Rxy sty()stx(i)=sti()Note that stx()always contains at most free variable(namely x).Proposition:For any basic hybrid formula,any Kripke model M,andany state w in M we have that:M,w?iffM|=stx()x w.Standard Translation:examplestx(ip i)p)=(stx(ip i)stx(p)=(stx(ip)stx(i)stx(p)=(stx(i

33、p)stx(i)Px=(stx(ip)i=x)Px=(sti(p)i=x)Px=(Pi i=x)PxIt should be clear from this examples that nominals have verymuch like first-order constants(or free variables).It should also bebecoming clear that basic hybrid logic essentially offers us a toolfor“adding naming and equality reasoning to modal logi

34、c”,or a“modal logic of equality for the elements in Kripke models”Standard Translation:examplestx(ip i)p)=(stx(ip i)stx(p)=(stx(ip)stx(i)stx(p)=(stx(ip)stx(i)Px=(stx(ip)i=x)Px=(sti(p)i=x)Px=(Pi i=x)PxIt should be clear from this examples that nominals have verymuch like first-order constants(or free

35、 variables).It should also bebecoming clear that basic hybrid logic essentially offers us a toolfor“adding naming and equality reasoning to modal logic”,or a“modal logic of equality for the elements in Kripke models”Standard Translation:examplestx(ip i)p)=(stx(ip i)stx(p)=(stx(ip)stx(i)stx(p)=(stx(i

36、p)stx(i)Px=(stx(ip)i=x)Px=(sti(p)i=x)Px=(Pi i=x)PxIt should be clear from this examples that nominals have verymuch like first-order constants(or free variables).It should also bebecoming clear that basic hybrid logic essentially offers us a toolfor“adding naming and equality reasoning to modal logi

37、c”,or a“modal logic of equality for the elements in Kripke models”Standard Translation:examplestx(ip i)p)=(stx(ip i)stx(p)=(stx(ip)stx(i)stx(p)=(stx(ip)stx(i)Px=(stx(ip)i=x)Px=(sti(p)i=x)Px=(Pi i=x)PxIt should be clear from this examples that nominals have verymuch like first-order constants(or free

38、 variables).It should also bebecoming clear that basic hybrid logic essentially offers us a toolfor“adding naming and equality reasoning to modal logic”,or a“modal logic of equality for the elements in Kripke models”Standard Translation:examplestx(ip i)p)=(stx(ip i)stx(p)=(stx(ip)stx(i)stx(p)=(stx(i

39、p)stx(i)Px=(stx(ip)i=x)Px=(sti(p)i=x)Px=(Pi i=x)PxIt should be clear from this examples that nominals have verymuch like first-order constants(or free variables).It should also bebecoming clear that basic hybrid logic essentially offers us a toolfor“adding naming and equality reasoning to modal logi

40、c”,or a“modal logic of equality for the elements in Kripke models”Standard Translation:examplestx(ip i)p)=(stx(ip i)stx(p)=(stx(ip)stx(i)stx(p)=(stx(ip)stx(i)Px=(stx(ip)i=x)Px=(sti(p)i=x)Px=(Pi i=x)PxIt should be clear from this examples that nominals have verymuch like first-order constants(or free

41、 variables).It should also bebecoming clear that basic hybrid logic essentially offers us a toolfor“adding naming and equality reasoning to modal logic”,or a“modal logic of equality for the elements in Kripke models”Standard Translation:examplestx(ip i)p)=(stx(ip i)stx(p)=(stx(ip)stx(i)stx(p)=(stx(i

42、p)stx(i)Px=(stx(ip)i=x)Px=(sti(p)i=x)Px=(Pi i=x)PxIt should be clear from this examples that nominals have verymuch like first-order constants(or free variables).It should also bebecoming clear that basic hybrid logic essentially offers us a toolfor“adding naming and equality reasoning to modal logi

43、c”,or a“modal logic of equality for the elements in Kripke models”Basic hybrid logic can specify Robinson Diagramsip says that the states labelled i bears the information p,whileip denies this.That is,we can specify how atomic properties aredistributed modally.ij says that the states labelled i and

44、j are identical,while ijsays they are distinct.That is,we can specify theories of stateequality modally.i3j says that the state labelled j is a successor of the statelabelled i,and i3j denies this.That is,we can specify theoriesof state succession modally.That is,we have all the tools needed to comp

45、letely describe models(thatis,what model theorists call Robinson diagrams).This makes life verystraightforward when it comes to proving completeness and interpolationresults.Hybrid reasoning and completenessWeve seen how basic hybrid logic works,and weve also seen howsome of its main ideas link clos

46、ely to ideas from first-order logic.Now for hybrid reasoning and completeness.Discuss the goals and problems of orthodox modal deduction.Present a hybrid tableau system for reasoning about arbitrarymodels.Show how this can be extended to hybrid tableau systems forspecial classes of models.Explain wh

47、y hybrid completeness works out sostraightforwardly.Round offby discussing further themes in hybrid deduction,including their implementation.Different models,different logicsKey fact about modal logic:when you work with different kinds ofmodels(graphs)the logic typically changes.For example:2p 2q 2(

48、p q)is valid on all models:its part of thebasic,universally applicable,logic.But 33p 3p is only valid on transitive graphs.Its notpart of the basic logic,rather its part of the special(stronger)logic that we need to use when working with transitive models.Modal deduction should be generalQuite right

49、ly,modal logicians have insisted on developingproof methods which are general that is,which can beeasily adapted to cope with the logics of many kinds ofmodels(transitive,reflexive,symmetric,dense,and so on).They achieve this goal by making use of Hilbert-style systems(that is,axiomatic systems).As

50、we noted earlier today,there is a basic axiomatic systems(called K)for dealing with arbitrary models.To deal with special classes of models,further axioms areadded to K.For example,adding 33p 3p as an axiomgives us the logic of transitive frames.Generality clashes with easy of useUnfortunately,Hilbe