1 Modal Logic CS112 Notes Modal Logic Part I

B ulletin of the S ection of L ogicVolume17/1(1988),pp.2–10reedition2005[original edition,pp.2–14]Ewa Or l owskaRELATIONAL INTERPRETATION OF MODAL LOGICS1.IntroductionThe purpose of the present paper is to show that modal propositional log-ics can be interpreted in a logic based on relational calculus.We consider languages with necessity operators[R],where R is an accessibility rela-tion expression representing an element of the algebra of binary relations (Tarski1941)with operations−,∪,∩,−1,◦.The relational logic is based on relational calculus enriched by operations of weakest prespecification(\) and weakest postspecification(/)introduced in Hoare and He Jifeng(1986) and investigated in He Jifeng et al(1986).The logic is an extension of the system introduced in Or l owska(1986)and investigated in Buszkowski and Or l owska(l986a,b).Let relations Q⊆Y×Z and R⊆X×Z be given.The weakest prespecification Q\R of Q to achieve R is the greatest relation P⊆X×Y such that P◦Q⊆R.Proposition1.1.Q\R is the weakest prespecification of Q to achieve R iff((x,y)∈Q\R iff(y,z)∈Q implies(x,z)∈R for all z).Let relations P⊆X×Y and R⊆X×Z be given.The weakest postspecification R/P of P to achieve R is the greatest relation Q⊆Y×Z such that P◦Q⊆R.Proposition1.2.R/P is the weakest postspecification of P to achieve R iff((y,z)∈R/P iff(x,y)∈P implies(x,z)∈R for all x).Relational Interpretation of Modal Logic3 2.Logic LREL of relationsWe define a formal language with expressions of the two kinds:relational expressions,interpreted as binary relations,and formulas,interpreted as schemes of sentences saying that a relation holds for a pair of objects. Expressions of the language are built up from symbols taken from the following pairwise disjoint sets:VAROB-a set of object variablesCONREL-a set of relational constants such that1,I∈CONREL {∪,∩,−,◦,−1,\,/}the set of relational operations.Set EREL of relational expressions is the smallest set including set CONREL of relational constants and closed with respect to relational operations.Set F ORREL of formulas is the set of expressions of the form xP y for x,y∈V AROB and P∈EREL.By a model we mean a system of the form M=(OB,{r P}P∈CONREL,m),where OB is a nonempty set of objects,for each P∈CONREL,r P is a binary relation in set OB,and m is a meaning function providing interpretation of relational expressions. We assume that function m satisfies the following conditions: m(P)=r P for any P∈CONREL,m(1)=OB×OB=1M,m(I)={(s,s):s∈OB}=I M,m(−P)=−m(P),m(P−1)=(m(P))−1,m(P∪Q)=m(P)∪m(Q),m(P∩Q)=m(P)∩m(Q),m(P◦Q)=m(P)◦m(Q),m(Q\R)=m(Q)\m(R),m(R/P)=m(R)/m(P).By a valuation we mean a function v:V AROB→OB which assigns objects to object variables.We say that in model M valuation v satisfies formula xP y whenever objects v(x)and v(y)stand in relation m(P):M,v sat xP y iff(v(x),v(y))∈m(P).We say that a formula F is true in a model M(|=M F)iffM,v sat F for all valuations v.A formula F is valid iffit is true in all models. We say that formulas F1,...,F n imply a formula F ifffor any model M if F1,...,F n are true in M,then F is true in M.4Ewa Or l owska Proposition2.1.(a)|=M xP y iffm(P)=1M(b)|=M x(1◦−P◦1)y iffm(P)=1M(c)|=M x(−P∪R)y iffm(P)⊆m(R)(d)|=M x((−P∪R)∩(−R∪P))y iffm(P)=m(R)(e)|=M x(1◦(−(R1∩...∩R n))◦1∪R)y iffm(R1)=1M,...,m(R n)= 1M imply m(R)=1M.Proposition2.2.(a)|=M x(−I∪P)y iffm(P)is reflexive(b)|=M x(−(I∩P))y iffm(P)is irreflexive(c)|=M x(−P∪P−1)y iffm(P)is symmetric(d)|=M x(−P∪−(P−1)∪I)y iffm(P)is antisymmetric(e)|=M x(−(P◦P)∪P)y iffm(P)is transitive(f)|=M x(P∪P−1∪I)y iffm(P)is connective(g)|=M x(P◦1)y iffm(P)is a total relation(h)|=M x(−(P−1◦P)∪I)y iffm(P)is a functionProposition2.3.(a)|=M x(1◦(I∩−P)◦1∪−R∪P◦R)y iffm(P)reflexive implies m(R)⊆m(P)◦m(R)(b)|=M x(1◦(I∩R)◦1∪−(R/1))y iffm(R)irreflexive implies m(R)/1M=03.Deduction systemsIn the present section we define deduction rules for the presented language. We follow the method developed in Rasiowa and Sikorski(1963)for the classical predicate calculus.The rules apply tofinite sequences of formulas, and they enable us to decompose formulas in a sequence into some simpler formulas.As a result of decomposition we obtain a single sequence or a pair of sequences.We admit the following rules:(∪)K,x(P∪Q)y,H K,xP y,xQy,H(−∪)K,x(−(P∪Q))y,HK,x(−P)y,H K,x(−Q)y,HRelational Interpretation of Modal Logic5(∩)K,x(P∩Q)y,H K,xP y,H K,xQy,H(−∩)K,x(−(P∩Q))y,H K,x(−P)y,x(−Q)y,H(−−)K,x(−−P)y,H K,xP y,H(−1)K,xP −1y,HK,yP x,H(−−1)K,x(−(P−1))y,H K,y(−P)x,H(◦)K,x(P◦Q)y,HK,xP z,H,x(P◦Q)y K,zQy,H,x(P◦Q)y where z is an arbitrary variable(−◦)K,x(−(P◦Q))y,HK,x(−P)z,z(−Q)y,Hwhere z is a variable which does not appear in any formula above the line(\)K,xQ\Ry,HK,y(−Q)z,xRz,Hwhere z is a variable which does not appear in any formula above the line(−\)K,x(−(Q\R))y,HK,yQz,H,x(−(Q\R))y K,x(−R)z,H,x(−Q\R))y where z is an arbitrary variable(/)K,xR/P y,HK,z(−P)x,zRy,Hwhere z is a variable which does not appear in any formula above the line(−/)K,x(−(R/P))y,HK,zP x,H,x(−(R/P))y K,z(−R)y,H,x(−(R/P))y where z is an arbitrary variable(symI)K,xIy,HK,yIx,xIy,H(tranI)K,xIy,HK,xIz,xIy,H K,zIy,xIy,Hwhere z is an arbitrary variable.6Ewa Or l owska In all the above rules K and H denotefinite or empty sequences of formulas.A sequence of formulas is said to be fundamental if it contains formulas of at least one of the following forms:(f1)xP y,x(−P)y for some P∈EREL and some x,y∈V AROB(f2)x1y for some x,y∈V AROB(f3)xIx for some x∈V AROB.Given a formula of the form xP y,where P ia a compound relational expression,we can decompose it by successive application of the rules.In the process of decomposition we form a tree whose vertices consist offinite sequences of formulas.We assume that sequences are read from left to right,and thefirst formula with a compound relational expression is a basis of decomposition.Each vertex of the decomposition tree has at most two successors.We stop decomposing formulas in a vertex after obtaining a fundamental sequence,or if none of the rules can be applied to the formulas in the vertex.Sequences satisfying these conditions are called end sequences of the tree.Proposition3.1.A formula F is valid iffthe decomposition tree of F is finite and all its end sequences are fundamental.4.Modal logic LMODWe consider a multimodal propositional language with a family of modal operators determined,by accessibility relations.Expressions of the lan-guage are constructed with symbols from the following pairwise disjoint sets:V ARP ROP–a set of propositional variablesCONAC–a set of accessibility relation constants{−,∪,∩,◦,−1}–the set of relational operations{¬,∨,∧,→,[]}–the set of propositional operationsSet EAC of relational expressions representing accessibility relations is the smallest set including CONAC and closed with respect to relational operations−,∪,∩,◦,−1.Set F ORMOD of modal formulas is the smallest set satisfying theRelational Interpretation of Modal Logic7 following conditions:V ARP ROP⊆F ORMODF,G∈F ORMOD imply¬F,F∨G,F∧G,F→G∈F ORMODF∈F ORMOD,R∈EAC imply[R]F∈F ORMOD.By model of a modal language we mean a system M=(ST, {r R}R∈CONAC,m),where ST is a nonempty set whose elements are called states,for each constant R∈CONAC,r R is a binary relation in set ST, and m is a meaning function satisfying the following conditions: m(p)⊆ST for p∈V ARROP,m(R)=r R for R∈CONAC,m(−R)=−m(R),m(R−1)=(m(R))−1,m(R∪S)=m(R)∪m(S),m(R∩S)=m(R)∩m(S),m(R◦S)= m(R)◦m(S).We say that in model M a state s satisfies a formula F(M,s sat F) iffthe following conditions are satisfied:M,s sat p iffs∈m(p)for p∈V ARP ROPM,s sat¬F iffnot M,s sat FM,s sat F∨G iffM,s sat F or M,s sat GM,s sat F∧G iffM,s sat F and M,s sat GM,s sat F→G iffM,s sat(¬F∨G)M,s sat[R]F ifffor all s ∈ST,(s,s )∈m(R)impliesM,s sat F.We say that a formula F is true ia a model M iffM,s sat F for all s∈ST.A formula F is valid in LMOD iffF is true in all models.A formula F is satisfiable iffthere are M and s such that M,s sat F.A formula F is unsatisfiable iffit is not satisfiable.5.Translation of modal language into rela-tional languageAssume that a one-to-one mapping t :CONAC∪V ARP ROP−→CONREL is given,assigning relational constants and propositional vari-ables and preserving1and I.We define translation function t:EAC∪8Ewa Or l owska F ORMOD→EREL assigning relational expressions to accessibility rela-tion expressions and modal formulas:t(R)=t (R)for R∈CONAC,t(−R)=−t(R),t(R−1=t(R)−1,t(R∪S)=t(R)∪t(S),t(R∩S)=t(R)∩t(S),t(R◦S)=t(R)◦t(S), t(p)=t (p)◦1for p∈V ARP ROP,t(¬F)=−t(F),t(F∨G)=t(F)∪t(G),t(F∧G)=t(F)∩t(G),t(F→G)=t(¬F∨G), t([R]F)=t(F)/t(R)−1.Proposition5.1.For any formula F and for any model M of modal logic LMOD there is a model M of logic LREL such that F is true in M iffxt(F)y is true in M .6.Logic of relations as a metasystem for modal logicsIn logic LREL we can prove both theorems and metatheorems of modal logics.Proposition6.1.(a)F is valid in LMOD iffxt(F)y is valid in LREL(b)F is not valid in LMOD iffx(1◦−t(F))y is valid in LREL(c)F is satisfiable in LMOD iffx(1◦t(F))y is valid in LREL(d)F is unsatisfiable in LMOD iffx(−t(F))y is valid in LREL.In logic LREL we can also express derivability of modal formulas from some other modal formulas.Proposition6.2.F1,...,F n imply F in LMOD iffx(1◦−(t(F1)∩...∩t(F n))◦1∪t(F))y is valid in LREL.Let P ROP be a property of relations,and let EP ROP(R)be a relational expression which reflects possession of P ROP by ly, EP ROP(R)represents universal relation iffR possesses P ROP.For ex-ample,if P ROP=reflexivity,then EP ROP(R)=−I∪R,since we have R is reflexive iffI⊆R iff−I∪R=1.Let R be an accessibility relation expression,and let F(R)be a formula of LMOD in which R occurs.Relational Interpretation of Modal Logic9 Proposition6.3.The following conditions are equivalent:Relation represented by R possesses P ROP implies F(R)is valid in LMOD,EP ROP(t(R))=1implies t(F(R))=1,x(1◦−EP ROP(t(R))◦1∪t(F(R)))y is valid in LREL.If we enrich the language of LMOD by sufficiency operators(Hum-berstone1983,Gargov et al1986)with semantics M,s sat[[R]]F ifffor all t∈ST:M,t sat F implies(s,t)∈m(R)then in the relational represen-tation we shall use the operation of weakest prespecification:t([[R]]F)= t(F)−1\t(R).Within the framework of relational logic we can easily deal with suf-ficiency operators determined by compound accessibility relations of the form−R,R−1,R∪S,R∩S,R◦S.Formulas with possibility operators<R>defined by the clause M,s sat <R>F iffthere is t∈ST such that(s,t)∈m(R)and M,t sat F can also be expressed in LREL.Their translation is as follows:t(<R>F)= t(R)◦t(F).Some operators used in dynamic logic(Harel1979)can be interpreted in LREL.For example,accessibility relation expression of the form F?, where F is a modal formula,whose interpretation in a model M is m(F?)= {(s,s)∈ST×ST:M,s sat F}should be translated as follows:t(F?)= t(I)∩t(F).Clearly,to translate formulas with modal operators of necessity,pos-sibility,and sufficiency into relations it is sufficient to use set-theoretical operations and composition and hence decomposition rules for/and\are redundant.However,it seems that these operations provide a direct and elegant representation of modal operators.References[1]W.Buszkowski and E.Or l owska,On the logic of data-base depen-dencies,Bulletin of the PAS34(1986a),Mathematics,pp.345–354.[2]W.Buszkowski and E.Or l owska,Relational calculus and data dependencies,ICS PAS Reports578(1986b),Warsaw.[3]G.Gargov,S.Passy,T.Tinchev,Modal environment for Boolean spaculations[in:] D.Skordev(ed)Mathematical Logic and Applica-10Ewa Or l owska tions,Proceedings of the1986Goedel Conference,Druzhba,Bulgaria, plenum Press,1986New York.[4] D.Harel,First order dynamic logic,Lecture Notes in Com-puter Science69(1979),Springer,Berlin,Heidelberg,New York.[5]He Jifeng,C.A.R.Hoare,J.Sanders,(Re)capturing the states of a process.Manuscript,Oxford University.[6] C.A.R.Hoare and He Jifeng,The weakest prespecification,Fun-damenta Informaticae IX(1986),Part I pp.51–84,Part II pp.217–252.[7]I.L.Humberstone,Inaccessible worlds,Notre Dame Journal of Formal Logic24(1983),pp.346–352.[8] E.Or l owska,Reasoning about database constraints,ICS PAS Reports543(1984),Warsaw.[9]H.Rasiowa and R.Sikorski,Mathematics of metamathemat-ics,Polish Scientific Publishers,1963Warsaw.[10] A.Tarski,On the calculus of relations,Journal of Symbolic Logic6(1941),pp.73–89.Polish Academy of SciencesP.O.Box2200–901WarsawPoland。

A Quantified Epistemic Logicfor Reasoning about Multi-Agent Systems∗F.Belardinelli Department of Computing Imperial College London180Queen’s GateLondon SW72AZF.Belardinelli@A.Lomuscio Department of Computing Imperial College London 180Queen’s GateLondon SW72AZA.Lomuscio@Categories and Subject DescriptorsF.4.1[Theory of Computation]:Mathematical Logic—modal logic;I.2.4[Artificial Intelligence]:Knowledge Rep-resentation—modal logic,predicate logicGeneral TermsLanguages,Theory.KeywordsEpistemic logic,First-order logic,Completeness.ABSTRACTWe investigate quantified interpreted systems,a semantics for multi-agent systems in which agents can reason about individuals,their properties,and the relationships among them.We analyse afirst-order epistemic language inter-preted on this semantics and show soundness and complete-ness of Q.S5n,an axiomatisation for these structures.1.INTRODUCTIONModal epistemic logic has been widely studied to rea-son about multi-agent systems(MAS),often in combina-tion with temporal modalities.The typical language extends propositional logic by adding n modalities K i representing the knowledge of agent i,as well as other modalities rep-resenting various mental states(explicit knowledge,beliefs, etc)and/or theflow of time.The use of modal propositional logic as a specification language requires little justification: it is a rather expressive language,well-understood from a theoretical point of view.Still,it is hard to counterargue the remark,often raised from practitioners in Software Engineering,that quantifica-tion in specifications is so natural and convenient that it really should be brought explicitly into the language.Even ∗The present research was supported by the Royal Society. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on thefirst page.To copy otherwise,to republish,to post on servers or to redistribute to lists,requires prior specific permission and/or a fee.AAMAS’07May14–182007,Honolulu,Hawai’i,USA.Copyright2007IFAAMAS.when working withfinite domains of individuals,without quantification one is forced to introduce ad-hoc propositions to emulate basic relations between individuals(as to express specifications like“the child of process p can send a message to all the processes that are allowed to invoke p”).In open MAS individuals may appear and disappear in the system at run-time,making the case for quantification even more compelling.Additionally,in a quantified modal language epistemic operators may be combined with quantifiers to express concepts such as de re/de dicto knowledge. However,the use offirst-order modal logic in MAS spec-ifications is normally frown upon by theoreticians.Why should we use an undecidable language when a decidable one does the job already?Is the price that quantification brings in justified?While these objections are certainly sensible, we believe their strength has been increasingly weakened by recent progress in the area of MAS verification[8,12,13]by model checking.In the model checking approach[1]we do not check whether a formula representing a specification is satisfiable in some model based on the completeness class, but simply whether a formula is true on the model represent-ing all possible evolutions of the system.While the former problem is undecidable forfirst-order modal logic(see[7]), the latter is decidable at least for some suitable fragments. This paper takes inspiration from the considerations above and aims at making progress on the subject offirst-order epistemic logic.The main contribution is the sound and complete axiomatisation of quantified interpreted systems (QIS)in Section5.QIS are an extension tofirst order of Interpreted Systems semantics,the usual formalism for epis-temic logic in MAS[4].While we are not aware of complete-ness results of this nature on the subject,quantified modal logic(QML)has been discussed in MAS settings before.In [4]QML and its Kripke semantics are briefly discussed.In [10]the authors introduce a quantified logic of belief with doxastic modalities indexed to terms of afirst-order lan-guage.In[14]a quantified temporal epistemic logic is dis-cussed.On related subjects,in[2,3]Cohen and Levesque develop afirst-order logic of belief and action with quantifi-cation over agents,although the semantics is not given in terms of computationally grounded structures[15].In all works above completeness is not tackled.This may be due to the technical difficulties associated with QML and the relatively poor status of the metatheoretical investiga-tion in comparison with the propositional case.We hope the present contribution will be thefirst in a line of work in which a systematic analysis of these logics is provided.2.SYSTEMS OF GLOBAL STATESThis paper is primarily concerned with the representation of knowledge in MAS,not their temporal evolution.Given this,we adopt the“static”perspective on the systems of global states[11],rather than their“dynamic”version[4]. More formally,consider a set L i of local states l i,l i,...,for each agent i∈A,and a set L e containing the states of the environment l e,l e,...;then define a system of global states as follows:Definition1.A system of global states S-or SGS in short-is a pair S,D such that S⊆L e×L1×...×L n and D is a non-empty domain of individuals.For s= l e,l1,...,l n ∈S,s i is equal to l i,for i∈A.We denote by SGS the class of the systems of global states. Remarks:This definition of SGS is grounded on two as-sumptions.First,the domain D of individuals is the same for every agent i,so all the agents reason about the same objects.This choice is justified by the external account of knowledge adopted in the framework of interpreted systems. Second,the domain D is assumed to be the same for every global state,i.e.no individual appears nor disappears in moving from one state to another.Again,this is also con-sistent with the external account of knowledge.We discuss further options in Section6.Finally,note that it can be the case that A⊆D.This means that the agents can reason about themselves,their properties and relationships.3.SYNTAX AND SEMANTICSFirst-order multi-modal formulas are defined on an alpha-bet containing the variables x1,x2,...,the n-ary functors f n1,f n2,...,and the n-ary predicative constants P n1,P n2,..., for n∈N,the identity=,the propositional connectives¬and→,the universal quantifier∀and the epistemic opera-tors K i,for every i∈A.Terms and formulas in the language L n are defined as follows:t::=x|f k(t1,...,t k)φ::=P k(t1,...,t k)|t=t |¬φ|φ→ψ|K iφ|∀xφRemarks:The symbols⊥,∧,∨,↔and∃are defined in the standard way.By t[ y/ t](resp.φ[ y/ t])we denote the term(resp.formula)obtained by simultaneously sub-stituting some,possibly all,free occurrences of y1,...,y n in t(resp.φ)with t1,...,t n,renaming bounded variables if necessary.By V ar we denote the set of variables in L n. We interpret the language L n on a system of global states S by means of a function I mapping the syntactic features of L n to the elements of S.Definition2.Given an SGS S,a quantified interpreted system-or QIS in short-is a pair P= S,I such that I(f k)is a k-ary function from D k to D;for every s∈S, I(P k,s)is a subset of D k and I(=,s)is the equality on D. Note that functors are interpreted rigidly.Letσbe an assignment,i.e.any function from V ar to D,the valuation Iσ(t)of a term t is inductively defined as follows:Iσ(y)=σ(y)Iσ(f k(t1,...,t k))=I(f k)(Iσ(t1),...,Iσ(t k))A variantσ`xa´of an assignmentσdiffers fromσat most onx and assigns element a∈D to x.Definition3(Satisfaction).The satisfaction relation |=forφ∈L n,s∈P and assignmentσis defined as follows: (Pσ,s)|=P k(t1,...,t k)iff Iσ(t1),...,Iσ(t k) ∈I(P k,s) (Pσ,s)|=t=t iffIσ(t)=Iσ(t )(Pσ,s)|=¬ψiff(Pσ,s)|=ψ(Pσ,s)|=φ→ψiff(Pσ,s)|=φor(Pσ,s)|=ψ(Pσ,s)|=K iψiffs i=s i implies(Pσ,s )|=ψ(Pσ,s)|=∀xψifffor every a∈D,(Pσ(x a),s)|=ψThe truth conditions for formulas containing⊥,∧,∨,↔,∃are defined as usual.A formulaφin L n is true at a state s iffit is satisfied at s by every assignmentσ;φis valid on a QIS P iffit is true at every state in P;φis valid on a SGS S iffit is valid on every QIS on S;φis valid on a class C of SGS iffit is valid on every SGS in C.4.EXPRESSIVENESSNote that in the language L n we can express an agent’s knowledge of properties and relationships among individu-als.Consider the following specifications:1.agent a knows that for every process x,agent b knowsthat there exists a precondition y,which has to befulfilled in order for x to start.2.agent a knows that there exists an input x for whichagent b does not know that every computation y oninput x fails.3.agent c knows that not every agent is identical to d;inparticular,she knows that she is not identical to d. These statements can be formalised as follows:1.K a∀x(Proc(x)→K b∃y(Pre(y)∧(St(x)→Fulfil(y))))2.K a∃x(Input(x)∧¬K b∀y(Comp(y)→Fails(x,y)))3.K c¬∀x(Ag(x)→x=agent-d)∧K c(agent-c=agent-d) Clearly,in this framework one can model the knowledge agents have about themselves.In addition,we retain all the expressive power of propositional epistemic logic.Further-more,we can now express the de re/de dicto distinction, that is,the difference between knowing something of some-one and knowing that someone is something.For instance, when we use an informal specification to say that,as far as a security controller is concerned,every user is authorised to access the site,one could interpret this as(hence implement it!)either de dicto,i.e.descriptively:a)the security controller knows that every user is autho-rised to access the site,or de re,i.e.prescriptively:b)for every user,the security controller knows that he is authorised to access the site.These two readings express different concepts.While these cannot be easily separated by means of a propositional lan-guage,in L n this is succintly done as follows:a)K SecCont∀x(Auth-user(x)→Access(x))b)∀x(Auth-user(x)→K SecCont Access(x))The difference in meaning between the two specifications is clear.For instance,the security controller not granting access to an authorised user u is a violation of(b),but not of(a),if he does not regard u to be an authorised user.5.AXIOMATISATIONThe system Q.S5n on the language L n is afirst-order multi-modal version of the normal propositional system S5. Hereafter we list its axioms;note that⇒is the inference relation between formulas.Definition4.The system Q.S5n on L n contains the fol-lowing schemes of axioms and inference rules:Taut every classic propositional tautologyDist K i(φ→ψ)→(K iφ→K iψ)T K iφ→φ4K iφ→K i K iφ5¬K iφ→K i¬K iφMPφ→ψ,φ⇒ψNecφ⇒K iφEx∀xφ→φ[x/t]Genφ→ψ[x/t]⇒φ→∀xψ,x not free inφId t=tFunc t=t →(t [x/t]=t [x/t ])Subst t=t →(φ[x/t]→φ[x/t ])It is easy to check that every axiom in Q.S5n is valid on any system of global states and its rules preserve valid-ity.We can also show that the axioms and inference rules in Q.S5n are sufficient to prove all the validities on SGS. This result is obtained by extending the completeness proofs forfirst-order modal logic in[6,9].By combining together soundness and completeness we obtain the main result of this paper.Theorem1.A formulaφis valid on the class SGS of systems of global states iffφis provable in Q.S5n.6.CONCLUSIONSIt is clear thatfirst-order modal formalisms offer expres-sivity advantages over propositional modal ones.However, the specialised literature has so far fallen short of a deep and systematic analysis of the machinery,even in the case of static epistemic logic.In this paper we believe we have made afirst attempt in this direction:the axiomatisation presented shows that the popular system S5n extends naturally to thefirst-order case.In carrying out this exercise we tried to remain as close as possible to the original epistemic logic’s semantics of interpreted systems,so thatfine grained specifications of MAS can be expressed as recent work on model checking interpreted systems demonstrates[5,13].Different extensions of the present framework seem pursu-ing.First of all,it seems interesting to relax the assumption on the domain of quantification and admit a different do-main D(s),for every state s.Further,we could assume a different domain of quantification D i(s)for every agent i in a state s.It would also be of interest to explore the com-pleteness issues resulting from term-indexing of the epis-temic operators[10].In an orthogonal dimension to the above another significant extension would be to add tem-poral operators to the formalism.This would pave the way for an exploration of axiomatisations for temporal/epistemic logic for MAS.7.REFERENCES[1]E.Clarke,O.Grumberg,and D.Peled.ModelChecking.MIT Press,Cambridge,Massachusetts,1999.[2]P.Cohen and H.Levesque.Intention is choice withcommitment.Artificial Intelligence,42:213–261,1990.[3]P.R.Cohen and H.J.Levesque.Rational interactionas the basis for communication.In P.R.Cohen,J.Morgan,and M.E.Pollack,editors,Intentions inCommunication.MIT Press,Cambridge,MA,1990. [4]R.Fagin,J.Halpern,Y.Moses,and M.Vardi.Reasoning about Knowledge.MIT Press,Cambridge,1995.[5]P.Gammie and R.van der Meyden.Mck:Modelchecking the logic of knowledge.In R.Alur andD.Peled,editors,CAV,volume3114of Lecture Notesin Computer Science,pages479–483.Springer,2004.[6]J.Garson.Quantification in modal logic.In Handbookof Philosophical Logic,volume2,pages249–307.D.Gabbay and F.Guenthner Eds.,1984.[7]I.M.Hodkinson,F.Wolter,and M.Zakharyaschev.Decidable fragment offirst-order temporal logics.Ann.Pure Appl.Logic,106(1-3):85–134,2000.[8]W.Hoek and M.Wooldridge.Tractable multiagentplanning for epistemic goals.In M.Gini,T.Ishida,C.Castelfranchi,and W.L.Johnson,editors,Proceedings of AAMAS’02,pages1167–1174.ACMPress,2002.[9]G.E.Hughes and M.J.Cresswell.A New Introductionto Modal Logic.Routledge,New York,1996.[10]A.Lomuscio and M.Colombetti.QLB:a quantifiedlogic for belief.In J.M¨u ller,M.Wooldridge,andN.Jennings,editors,Proceedings of ATAL-96,volume 1193of Lecture Notes in AI.Springer-Verlag,Heidelberg,1996.[11]A.Lomuscio and M.Ryan.On the relation betweeninterpreted systems and kripke models.In Springerlecture notes in AI,volume1441,1997.[12]J.-J.C.Meyer and W.Hoek.Epistemic Logic for AIand Computer Science,volume41of CambridgeTracts in Theoretical Computer Science.CambridgeUniversity Press,1995.[13]F.Raimondi and A.Lomuscio.Automatic verificationof multi-agent systems by model checking via OBDDs.Journal of Applied Logic,2005.To appear in Specialissue on Logic-based agent verification.[14]M.Wooldridge.The logical modelling of computationalmulti-agent systems.PhD thesis,University ofManchester,Faculy of Technology,1992.[15]putationally grounded theories ofagency.In E.Durfee,editor,Proceedings of ICMAS,International Conference of Multi-Agent Systems,pages13–22.IEEE Press,2000.。

Logics for Knowledge RepresentationBernhard NebelAlbert-Ludwigs-Universit¨a t Freiburg,Germany1IntroductionKnowledge representation and reasoning plays a central role in Artificial Intelli-gence.Research in Artificial Intelligence(henceforth AI)started off by trying to identify the general mechanisms responsible for intelligent behavior.However,it quickly became obvious that general and powerful methods are not enough to get the desired result,namely,intelligent behavior.Almost all tasks a human can per-form which are considered to require intelligence are also based on a huge amount of knowledge.For instance,understanding and producing natural language heavily relies on knowledge about the language,about the structure of the world,about social relationships etc.One way to address the problem of representing knowledge and reasoning about it is to use some form of logic.While this seems to be a natural choice,it took a while before this“logical point of view”became the prevalent approach in the area of knowledge representation.Below,we will give a brief sketch of how thefield of knowledge representation evolved and what kind logical methods have been used. Int.Encyc.Social and Behavioral Sciences27February2001In particular,we will argue that the important point about using formal logic is the logical method.2Logic-Based Knowledge Representation:A Historical AccountMcCarthy(1968)stated very early on that mathematical,formal logic appears to be a promising tool for achieving human-level intelligence on computers.In fact, this is still McCarthy’s(2000)vision,which he shares with many researchers in AI.However,in the early days of AI,there were also a number of researchers with a completely different opinion.Minsky(1975),for example,argued that knowl-edge representation formalisms should beflexible and informal.Moreover,he ar-gued that the logical notions of correctness and completeness are inappropriate in a knowledge representation context.While in those days heated arguments of the suitability of logic were exchanged,by the end of the eighties,the logical perspective seem to have gained the upper hand (Brachman1990).During the nineties almost all research in the area of knowledge representation and reasoning was based on formal,logical methods as demonstrated by the papers published in the bi-annual international conference on Principles of Knowledge Representation and Reasoning,which started in1989.It should be noted,however,that two perspectives on logic are possible.Thefirst perspective,taken by McCarthy(1968),is that logic should be used to represent knowledge.That is,we use logic as the representational and reasoning tool insidethe computer.Newell(1982)on the other hand proposed in his seminal paper on the knowledge level to use logic as a formal tool to analyze knowledge.Of course, these two views are not incompatible.Furthermore,once we accept that formal logic should be used as a tool for analyzing knowledge,it is a natural consequence to use logic for representing knowledge and for reasoning about it as well.3Knowledge Representation Formalisms and Their SemanticsSaying that logic is used as the main formal tool does not say which kind of logic is used.In fact,a large variety of logics(Gabbay,Hogger and Robinson1995)have been employed or developed in order to solve knowledge representation and rea-soning problems.Often,one started with a vaguely specified problem,developed some kind knowledge representation formalism without a formal semantics,and only later started to provide a formal ing this semantics,one could then analyze the complexity of the reasoning problems and develop sound and complete reasoning algorithms.I will call this the logical method,which proved to be very fruitful in the past and has a lot of potential for the future.3.1Description LogicsOne good example for the evolution of knowledge representation formalisms is the development of description logics,which have their roots in so-called struc-tured inheritance networks formalisms such as KL-ONE(Brachman1979).These networks were originally developed in order represent word meanings.A conceptnode connects to other concept nodes using roles.Moreover,the roles could be structured as well.These networks permits for,e.g.,the definition of the concept of a bachelor.Later on,these structured inheritance networks were formalized as so-called con-cept languages,terminological logics,or description logics.Concepts were inter-preted as unary predicates,roles as binary relations,and the connections between nodes as so-called value restrictions.This leads for most such description logics to a particular fragment offirst-order predicate logic,namely,the fragment.In this fragment only two different variable symbols are used.As it turns out,this is a decidable fragment offirst-order logic.However,some of the more involved description logics go beyond.They con-tain,e.g.,relational composition or transitive closure.As it turns out,such descrip-tion logics can be understood as variants of multi-modal logics(Schild1991),and decidability and complexity results from these multi-modal logics carry over to the description logics.Furthermore,description logics are very close to feature log-ics as they are used in unification-based grammars.In fact,description logics and feature logics can be viewed as members of the same family of representation for-malisms(Nebel and Smolka1990).All these insights,i.e.,determination of decidability and complexity as well as the design of decision algorithms(e.g.Donini,Lenzerini,Nardi and Nutt1991),are based on the rigorous formalization of the initial ideas.In particular,it is not justone logic that it is used to derive these results,but it is the logical method that led to the success.One starts with a specification of how expressions of the language or formalism have to be interpreted in formal terms.Based on that one can specify when a set of formulae logically implies a formula.Then one can start tofind similar formalisms(e.g.modal logics)and prove equivalences and/or one can specify a method to derive logically entailed sentences and prove them to be correct and complete.3.2Nonmonotonic LogicsAnother interesting area where the logical method has been applied is the devel-opment of the so-called non-monotonic logics.These are based on the intuition that sometimes a logical consequence should be retracted if new evidence becomes known.For example,we may assume that our car will not be moved by somebody else after we have parked it.However,if new information becomes known,such as the fact that the car is not at the place where we have parked it,we are ready to drop the assumption that our car has not been moved.This general reasoning pattern was used quite regularly in early AI systems,but it took a while before it was analyzed from a logical point of view.In1980,a special issue of the Artificial Intelligence journal appeared,presenting different ap-proaches to non-monotonic reasoning,in particular Reiter’s(1980)default logic and McCarthy’s(1980)circumscription approach.A disappointing fact about nonmonotonic logics appears to be that it is very difficult to formalize a domain such that one gets the intended conclusions.In particular,in the area of reasoning about actions,McDermott(1987)has demonstrated that the straightforward formalization of an easy temporal projection problem(the“Yale shooting problem”)does not lead to the desired consequences.However,it is pos-sible to get around this problem.Once all underlying assumptions are spelled out, this and other problem can be solved(Sandewall1994).It took more than a decade before people started to analyze the computational com-plexity(of the propositional versions)of these logics.As it turned out,these log-ics are usually somewhat more difficult than ordinary propositional logic(Gottlob 1992).This,however,seems tolerable since we get much more conclusions than in standard propositional logic.Right at the same time,the tight connection between nonmonotonic logic and belief revision(G¨a rdenfors1988)was noticed.Belief revision–modeling the evolution of beliefs over time–is just one way to describe how the set of nonmonotonic consequences evolve over time,which leads to a very tight connection on the formal level for these two forms of nonmonotonicity(Nebel1991).Again,all these results and insights are mainly based on the logical method to knowledge representation.4OutlookThe above description of the use of logics for knowledge representation is nec-essarily incomplete.For instance,we left out the area of qualitative temporal and spatial reasoning completely.Nevertheless,one should have got an idea of how log-ics are used in the area of knowledge representation.As mentioned,it is the idea of providing knowledge representation formalisms with formal(logical)semantics that enables us to communicate their meaning,to analyze their formal properties, to determine their computational complexity,and to devise reasoning algorithms.While the research area of knowledge representation is dominated by the logical approach,this does not mean that all approaches to knowledge representation must be based on logic.Probabilistic(Pearl1988)and decision theoretic approaches, for instance,have become very popular lately.Nowadays a number of approaches aim at unifying decision theoretic and logical accounts by introducing a qualita-tive version of decision theoretic concepts(Benferhat,Dubois,Fargier,Prade and Sabbadin2000).Other approaches(Boutilier,Reiter,Soutchanski and Thrun2000) aim at tightly integrating decision theoretic concepts such as Markov decision pro-cesses with logical approaches,for instance.Although this is not pure logic,the two latter approaches demonstrate the generality of the logical method:specify the formal meaning and analyze!BibliographyAllen,J. A.,Fikes,R.and Sandewall, E.(eds):1991,Principles of Knowledge Representation and Reasoning:Proceedings of the2nd International Conference(KR-91),Morgan Kaufmann,Cambridge,MA.Benferhat,S.,Dubois,D.,Fargier,H.,Prade,H.and Sabbadin,R.:2000,Decision, nonmonotonic reasoning and possibilistic logic,in Minker(2000),pp.333–360. Boutilier,C.,Reiter,R.,Soutchanski,M.and Thrun,S.:2000,Decision-theoretic,high-level agent programming in the situation calculus,Proceedings of the17th National Conference of the American Association for Artificial Intelligence(AAAI-2000),MIT Press,Austin,TX.Brachman,R.J.:1979,On the epistemological status of semantic networks,in N.V.Findler (ed.),Associative Networks:Representation and Use of Knowledge by Computers, Academic Press,New York,NY,pp.3–50.Brachman,R.J.:1990,The future of knowledge representation,Proceedings of the8th National Conference of the American Association for Artificial Intelligence(AAAI-90),MIT Press,Boston,MA,pp.1082–1092.Donini,F.M.,Lenzerini,M.,Nardi,D.and Nutt,W.:1991,The complexity of concept languages,in Allen,Fikes and Sandewall(1991),pp.151–162.Gabbay,D.M.,Hogger,C.J.and Robinson,J.A.(eds):1995,Handbook of Logic in Artificial Intelligence and Logic Programming–Vol.1–5,Oxford University Press, Oxford,UK.G¨a rdenfors,P.:1988,Knowledge in Flux—Modeling the Dynamics of Epistemic States, MIT Press,Cambridge,MA.Gottlob,G.:1992,Complexity results for nonmonotonic logics,Journal for Logic and Computation2(3),397–425.McCarthy,J.:1968,Programs with common sense,in M.Minsky(ed.),Semantic Information Processing,MIT Press,Cambridge,MA,pp.403–418.McCarthy,J.:1980,Circumscription—a form of non-monotonic reasoning,Artificial Intelligence13(1–2),27–39.McCarthy,J.:2000,Concepts of logical AI,in Minker(2000),pp.37–58. McDermott,D.V.:1987,A critique of pure reason,Computational Intelligence3(3),151–160.Minker,J.(ed.):2000,Logic-Based Artificial Intelligence,Kluwer,Dordrecht,Holland. Minsky,M.:1975,A framework for representing knowledge,in P.Winston(ed.),The Psychology of Computer Vision,McGraw-Hill,New York,NY,pp.211–277. Nebel,B.:1991,Belief revision and default reasoning:Syntax-based approaches,in Allen et al.(1991),pp.417–428.Nebel,B.and Smolka,G.:1990,Representation and reasoning with attributive descriptions, in K.-H.Bl¨a sius,U.Hedtst¨u ck and C.-R.Rollinger(eds),Sorts and Types in Artificial Intelligence,V ol.418of Lecture Notes in Artificial Intelligence,Springer-Verlag, Berlin,Heidelberg,New York,pp.112–139.Newell,A.:1982,The knowledge level,Artificial Intelligence18(1),87–127.Pearl,J.:1988,Probabilistic Reasoning in Intelligent Systems:Networks of Plausible Inference,Morgan Kaufmann,San Francisco,CA.Reiter,R.:1980,A logic for default reasoning,Artificial Intelligence13(1),81–132. Sandewall,E.:1994,Features and Fluents,Oxford University Press,Oxford,UK. Schild,K.:1991,A correspondence theory for terminological logics:Preliminary report, Proceedings of the12th International Joint Conference on Artificial Intelligence (IJCAI-91),Morgan Kaufmann,Sydney,Australia,pp.466–471.。

Journal of Logic,Language,and Information7:228–229,1998.228 Book ReviewLogic for Applications,Anil Nerode and Richard A.Shore,Graduate Texts in Computer Science, New York:Springer-Verlag,1997(2nd edition).Price:DM78.00,xiii+438pages,Index of symbols, Index of terms,ISBN:0-387-94893-7.In this impressive monograph,onefinds a thorough approach to logic infive chapters,organised along the following topics:Propositional and Predicate Logic,PROLOG,Modal and Intuitionistic Logic.Then,there is a sixth chapter(Elements of Set Theory),which,according to the diagram of dependencies between chapters,can be read and studied more or less independently from the other chapters.Appendix A provides a historical overview of logic and the foundations of mathematics(to appreciate this fully,the reader might also want to read thefirst six sections of the chapter on set theory),whereas Appendix B provides a genealogical database of PROLOG facts of the form “fatherof(a,b),”based on the Chronicles from the Hebrew Bible.These facts are used for various programming problems and exercises.Finally,the book contains an extensive bibliography,ordered by subject,and an index of symbols and one of terms.Moreover,exercises are provided at the end of each section,and each chapter ends with“Suggestions for Further Reading.”Whereas a computer scientist’s approach to logic is mirrorred in tableaux proofs,resolution and unification in thefirst two chapters,in Chapter III on PROLOG the real computational application starts with the specialization of resolution to Horn clauses.Negation as failure is then used as a bridge to a brief introduction to nonmonotonic logic.In spite of this single section on the topic(one nonmontonic formal system is introduced,similar to default logic),the authors are able to apply their setup to stable models.Chapters IV and V are devoted to nonclassical logics that are important for reasoning about computation:Intuitionistic and Modal Logic.The second edition of1997differs from the1993first edition in having the above mentioned Chapter VI on set theory.This chapter can be“either used as a reference to standard set-theoretic notations and concepts”but is“also a self-contained introduction to axiomatic set theory.”Thefirst six sections of this chapter treat standard notions from elementary set theory like functions, relations,orderings(the concept of order and,more specifically,tree,is also introduced in Section I.1) and sequences,whereas the remainingfive sections are devoted to transfinite induction,ordinals, cardinals and variations on the axiom of choice.Of course,in adding a specific foundational chapter, dangers of bootstrapping problems always arise.For instance,in order to formalize set theory,some notation from predicate logic is already presumed.Another,more dangerous example is given by the treatment of the principle of induction.In Section I.2,it is demonstrated how to perform a proof by induction on the structure of formulas.It is left as an exercise in Chapter I to show that this method can be related to the procedure of induction on numbers.However,the latter procedure is only defined in Section VI.4,in a rather abstract setting, that of inductive sets.According to its cover the book is“afirst introduction to mathematical logic[]no previous exposure to logic is assumed.”The introduction says that the book aims at upper level undergrad-uate and beginning graduate students of mathematics or computer science.I like to underscore that such students should at least be familiar with some mathematical notation and also some standardBOOK REVIEW229 arguments in reasoning.In my(Dutch)context of teaching logic,I see a tendency to introduce logic in a semi-formal way:students should play with reasoning patterns,get experienced with manipulations on quantifier sequences and should be able to easily come up with counterexamples for incorrect arguments.The focus of the book under review is not so much on these techniques,and personally,I would prefer to use it in an advanced logic class.The book is definitely written in the spirit of what the authors see as the applications of logic to computer science:instead of reasoning patterns,logic is about resolution theorem proving and deduction as computation.Models typically have ground terms in their domain,and attention for implementation issues(searching and backtracking,control of implementation,termination condi-tions)is justified in such a setup.I am particularly excited about the chapter on PROLOG;I am not aware of any comparably thorough and still accessible approach in thisfield.Thefirstfive sections of this chapter are very rigid and clear,extensive proofs are provided(completeness of several forms of resolution,including lifting and independence lemmas).These rather hard theoretical results are accompanied with several examples and SLD-trees.And if one decides to give a course on logic programming,Chapters I and II seem to be suitable for putting the student in the“right logical mood.”I doubt whether I would use these chapters as afirst introduction to logic,though.It is generally accepted that modal and intuitionistic logic are important for computer scientists, but I feel that in Chapters IV and V this importance is only mentioned,not really demonstrated. What kind of reasoning is offered by dynamic logic?How is epistemic logic exactly used?What are the mechanisms of constructive proof checkers and reasoning systems?How natural are proofs in a system like NUPRL?All in all,the book seems a good buy.If not for students in computer science,it is for teachers in this and related areas(expert systems,AI),because of its composition,the thoroughness of proofs and the many valuable references for further reading.Wiebe van der HoekDepartment of Computer ScienceUtrecht UniversityP.O.Box800893508TB UtrechtThe NetherlandsE-mail:************.nl。

l o g i c使用快捷键使用方法本页仅作为文档封面，使用时可以删除This document is for reference only-rar21year.March以前用过NUENDO等软件，Logic Pro 9的快捷键适应不了，怎么设置快捷键？启动Logic Pro 9，点击桌面左上角Logic Pro菜单，找到Preferences,找到key commands，在这里设置。

这里有一个我已经改好的快捷键预设，仿NUENDO的，可下载导入。

方法：在key commands窗口左上角，找到Option下拉菜单。

选择Import....，完成即可。

Logic Pro 9录音以后再录音，怎么会“顿”一下？在Logic Pro 9底部，transport (传送条）上，在录音按钮上单击鼠标右键，勾选“punch on the fly",好了，整个世界清净了。

我想对单个音频/MIDI事件进行非破坏性的移调处理怎么做？选择你要处理的音频/MIDI事件，在界面最左边Inspctor区域找到Transposition，输入数值：移高半音输入1，降低半音输入-1，以此类推。

在Logic Pro 9中怎样精细制作渐快、渐慢速度a 首先在刻度尺上选择你要变速的范围。

b将播放光标定位到范围的最右边c按键盘上的“T”键，打开LIST窗口d点击Create，程序将在播放光标位置，创建新的速度标记e在TEMPO栏下，输入你想要的新速度f在这个窗口上方，找到Options下来菜单，找到Tempo operations，在curve type出选择适合的渐变模式，如果从此以后就用新的速度，那么勾选“Continue with New Tempo",如果变速后还想马上回到原有速度则不要勾选，注意density这个下拉菜单，它可以让你的变速曲线像楼梯一样有棱有角，也可让曲线像丝绸一般顺滑。

g调整完了，点”Apply”，试听。

will与be going to的多维度意义对比情态动词意义研究一直是语言学长期以来探讨的问题.。

它不仅有逻辑情态分类语义层面的研究，而且还有认知语用层面的研究.。

本文从逻辑意义对英语情态动词will和半情态动词be going to的意义进行了不同维度的比较研究.。

1 . 引言情态动词意义研究可谓是由来已久，著说颇多.。

从分析来看，主要有语义学和语用学两个角度.。

从语义学角度来分析情态动词意义的研究认为，由于情态动词在不同的句子中可能表达多重意义，因而情态动词是一词多义.。

从语用学角度来看，作为话语的含有情态动词的句子只是用语言编码的信息输入.。

语用推导的关键在于句子本身意义和语境信息之间的关系，含有情态动词的话语的理解要取决于情态动词提供的关于该关系的信息.。

因此，情态动词可以看作有某种统一意义：它表达了话语其他部分所表达的句义和语境之间的关系.。

目前，国外已有很多文章对情态动词will和半情态动词be going to的意义进行了比较研究.。

其中具有代表性的有：Coates（1983）按照语义逻辑范畴分类，分别对will和be going to进行语义阐释和比较；Haegeman（1989），Klinge（1993），Nicolle（1997）则是从语用角度对这两个词进行对比研究.。

本文从逻辑意义和关联理论框架下的语用认知各个不同的方面对will和be going to的意义进行了比较研究.。

2 . 根源意义与推测意义从语义学上的逻辑意义来看，情态动词是一词多义的，同一情态动词可能会在不同的句子中表达不同的意思.。

从20世纪70年代开始不少语言学家便倾向于认为英语情态动词是逻辑学中情态范畴（logic modality）的语言表现形式.。

英语情态动词的意义可以根据情态逻辑（modal logic）分为根源意义（root meaning）和推测意义（epistemic meaning）.。

英语情态动词will和be going to都能表达根源意义和推测意义.。