Decidable Reasoning in a Modi?ed Situation Calculus
Yilan Gu
Dept.of Computer Science University of Toronto
10King’s College Road Toronto,ON,M5S3G4,Canada Email:yilan@https://www.doczj.com/doc/fb740370.html,
Mikhail Soutchanski Department of Computer Science Ryerson University
245Church Street,ENG281 Toronto,ON,M5B2K3,Canada Email:mes@scs.ryerson.ca
Abstract
We consider a modi?ed version of the situation cal-
culus built using a two-variable fragment of the
?rst-order logic extended with counting quanti?ers.
We mention several additional groups of axioms
that can be introduced to capture taxonomic rea-
soning.We show that the regression operator in this
framework can be de?ned similarly to regression in
the Reiter’s version of the situation https://www.doczj.com/doc/fb740370.html,ing
this new regression operator,we show that the pro-
jection and executability problems are decidable in
the modi?ed version even if an initial knowledge
base is incomplete and open.For an incomplete
knowledge base and for context-dependent actions,
we consider a type of progression that is sound with
respect to the classical progression.We show that
the new knowledge base resulting after our progres-
sion is de?nable in our modi?ed situation calculus
if one allows actions with local effects only.We
mention possible applications to formalization of
Semantic Web services.
1Introduction
The situation calculus is a popular and well understood pred-icate logic language for reasoning about actions and their ef-fects[Reiter,2001].It is used to provide a well-de?ned se-mantics for Web services and a foundation for a high-level programming language Golog[Reiter,2001;McIlraith and Son,2002].However,because the situation calculus is for-mulated in a general predicate logic,reasoning about effects of sequences of actions is undecidable(unless some restric-tions are imposed on the theory that axiomatizes the initial state of the world).The?rst motivation for our paper is intention to overcome this dif?culty.We propose to use a two-variable fragment FO2of the?rst-order logic(FOL)as a foundation for a modi?ed situation calculus.Because the sat-is?ability problem in this fragment is known to be decidable (it is in NE XP T IME),we demonstrate that by reducing rea-soning about effects of actions to reasoning in this fragment, one can always guarantee decidability.The second motiva-tion for our paper comes from description logics.Description Logics(DLs)[Baader et al.,2003]are a well-known family of knowledge representation formalisms,which play an im-
portant role in providing the formal foundations of several
widely used Web ontology languages including OWL in the
area of the Semantic Web.Many expressive DLs can be trans-lated to FO2and offer considerable expressive power going
far beyond propositional logic,while ensuring that reasoning
is decidable[Borgida,1996].DLs have been mostly used to
describe static knowledge bases.However,several research
groups consider formalization of actions using DLs or exten-
sions of DLs.Following the key observation that reasoning
about complex actions can be carried in a fragment of the
propositional situation calculus,[Giacomo et al.,1999]give
an epistemic extension of DLs to provide a framework for the
representation of dynamic systems.However,the representa-
tion and reasoning about actions in this framework are strictly
propositional,which reduces the representation power of this
framework.In[Baader et al.,2005],Baader et al.provide
another proposal for integrating description logics and ac-
tion formalisms.They take the well known description logic A L CQ IO(and its sub-languages)as foundation and show that the complexity of executability and projection problems(two
basic reasoning problems for possibly sequentially composed
actions)coincides with the complexity of standard DL rea-
soning.However,actions(services)are represented in their
paper meta-theoretically,not as?rst-order(FO)terms.This
can potentially lead to some complications when speci?ca-
tions of other reasoning tasks(e.g.,planning)will be consid-
ered because it is not possible to quantify over actions in their
framework.In our paper,we take a different approach and
represent actions as FO terms,but achieve integration of tax-
onomic reasoning and reasoning about actions by restricting
the syntax of the situation calculus and by introducing addi-
tional axioms to represent a taxonomy.
Because after doing longer and longer sequences of ac-
tions,solving projection problems becomes increasingly
more dif?cult,it is bene?cial to progress the initial incom-
plete knowledge base(KB)to represent the current state of
the world.Then,the subsequent projection problems can be
solved with respect to a new progressed KB.The task of com-
puting a progressed KB is called the progression problem.
Our paper is structured as follows.In Section2,we brie?y
review the Reiter’s situation calculus and the extension of FO2with counting quanti?ers.In Section3we discuss de-tails of our proposal:a modi?ed situation calculus.In Section
4we consider an extension of regression (the main reasoning mechanism in the situation calculus).Finally,in Section 5we discuss the progression problem and in Section 6we discuss brie?y other related approaches to reasoning about actions.
2Background
The situation calculus (SC)L sc is a predicate language for axiomatizing dynamic systems.All dialects of the SC L sc include three disjoint sorts:actions ,situations and objects .Actions are FO terms consisting of an action function sym-bol and its arguments.Actions change the world.Situa-tions are FO terms which denote world histories.A distin-guished constant S 0is used to denote the initial situation ,and function do (a,s )denotes the situation that results from performing action a in situation s .Every situation corre-sponds uniquely to a sequence of actions.Objects are FO terms other than actions and situations that depend on the domain of application.Fluents are relations or func-tions whose values may vary from one situation to the next.Normally,a ?uent is denoted by a predicate or function sym-bol whose last argument has the sort situation.For example,F ( x ,do ([α1,···,αn ],S 0))represents a relational ?uent in the situation do (αn ,do (···,do (α1,S 0)···)resulting from execution of ground action terms α1,···,αn in S 0.We do not consider functional ?uents in this paper.
The SC includes the distinguished predicate P oss (a,s )to characterize actions a that are possible to execute in s .For any SC formula φand a term s of sort situation,we say φis a formula uniform in s iff it does not mention the predicates P oss ,it does not quantify over variables of sort situation,it does not mention equality on situations,and whenever it men-tions a term of sort situation in the situation argument position of a ?uent,then that term is s (see [Reiter,2001]).If φ(s )is a uniform formula and the situation argument is clear from the context,sometimes we suppress the situation argument and write this formula simply as φ,and also introduce a notation φ[s ]to represent the SC formula obtained by restoring situa-tion s back to all the ?uents and/or P oss predicates (if any)in φ.It is obvious that φ[s ]is uniform in s .
A basic action theory (BAT)D in the SC is a set of axioms written in L sc with the following ?ve classes of axioms to model actions and their effects [Reiter,2001]:action precon-dition axioms D ap ,successor state axioms (SSAs)D ss ,initial theory D S 0,unique name axioms D una ,domain independent foundational axioms for situations Σ.
Suppose that D =D una ∪D S 0∪D ap ∪D ss ∪Σis a BAT,α1,···,αn is a sequence of ground action terms,and G (s )is a uniform formula with one free variable s .One of the most important reasoning tasks in the SC is the projection problem,that is,to determine whether D |=G (do ([α1,···,αn ],S 0)).Another basic reasoning task is the executabil-ity problem.Let executable (do ([α1,···,αn ],S 0))be an abbreviation of the formula P oss (α1,S 0)∧ n
i =2P oss (αi ,do ([α1,···,αi ?1],S 0)).
Then,the executability problem is to determine whether D |=executable (do ([α1,···,αn ],S 0)).Planning and high-level program execution are two important settings where the executability and projection problems arise natu-
rally.Regression is a central computational mechanism that forms the basis for automated solution to the executability and projection tasks in the SC [Reiter,2001].A recursive de?nition of the regression operator R on any regressable formula φis given in [Reiter,2001].We use notation R [φ]to denote the formula that results from eliminating P oss atoms in favor of their de?nitions as given by action precondition axioms and replacing ?uent atoms about do (α,s )by logically equivalent expressions about s as given by SSAs repeatedly until it cannot make such replacement any further.The formula G (do ([α1,···,αn ],S 0))is a particularly simple example of a regressable formula because it is uniform in do ([α1,···,αn ],S 0)),but generally,regressable formulas can mention several different ground situation terms.The re-gression theorem shows that one can reduce the evaluation of a regressable formula φto a FOL theorem proving task in the initial theory together with unique names axioms for actions:
D |=φiff D S 0∪D una |=R [φ].
This fact is the key result for our paper:it demonstrates that an executability or a projection task can be reduced to a FOL theorem proving task.However,because D S 0is an arbitrary FO theory,this type of reasoning is undecidable.Two of the most common ways to overcome this dif?culty is to introduce the closed world assumption or introduce the domain closure assumption (i.e.,assume the domain is ?nite).In many application domains these assumptions are unrealistic.Therefore,we consider a version of the SC formulated in FO 2,or in C 2.
Two-variable FO logic FO 2is the fragment of ordinary FO logic (with equality),whose formulas only use no more than two variable symbols x and y (free or bound).Two-variable FO logic with counting C 2extends FO 2by allowing FO counting quanti?ers ?≥m and ?≤m for all m ≥1.[Pa-cholski et al.,1997]show that satis?ability problem for C 2is decidable and recently [Pratt-Hartmann,2005]proves that this problem is in NE XP T IME even when counting quanti?ers are coded succinctly.See additional background on DLs and discussion of connections between DLs with C 2in [Baader et al.,2003;Borgida,1996;Gu and Soutchanski,2006].
3
Modeling Dynamic Systems in a Modi?ed Situation Calculus
In this section,we consider dynamic systems formulated in a modi?cation of the language of the SC so that it can be con-sidered as an extension to C 2(with an additional situation ar-gument).1The key idea is to consider a syntactic modi?cation of the SC such that the executability and projection problems are guaranteed to be decidable as a consequence of the de-cidability of the satis?ability problem in C 2.Moreover,since the modi?ed SC has strong connections with description log-ics,which will be explained in detail below,we will denote this language as L DL sc .
First of all,the three sorts in L DL sc (i.e.,actions,situations and objects)are the same as those in L sc ,except that they
1
The reason that we call it a ”modi?ed”SC rather than a ”re-stricted”SC is that we extend the SC with other features,such as adding acyclic TBox axioms to basic action theories.
obey the following restrictions:(1)all terms of sort object are variables (x and y )or constants,i.e.,object functional symbols are not allowed;(2)all action functions include no more than two arguments.Each argument of any term of sort action is either a constant or an object variable (x or y );(3)variable s of sort situation and/or variable a of sort action are the only additional variables being allowed in D ?Σ?D una in addition to variables x ,y .Second,any ?uent in L DL sc is a predicate either with two or with three arguments (including the one of sort situation).We call ?uents with two arguments (dynamic)concepts ,and call ?uents with three arguments (dynamic)roles .In L DL sc ,(static)concepts (i.e.,unary predicates with no situation ar-gument)and (static)roles (i.e.,binary predicates with no sit-uation argument),if any,are considered as unchangeable tax-onomic properties and unchangeable classes of an application domain.Moreover,each concept (static or dynamic)can be either primitive or de?ned .
Third,apart from the standard FO logical symbols ∧,∨and ?,with the usual de?nition of a full set of connectives
and quanti?ers,L DL sc also includes counting quanti?ers ?≥m
and ?≤m for all m ≥1.Equality =is allowed in L DL sc .
The dynamic systems we are dealing with here sat-isfy the open world assumption (OW A):what is not stated explicitly is currently unknown rather than false.In this paper,the dynamic systems we are interested in can be formalized as a basic action theory (BAT)D using the following seven groups of axioms in L DL sc :D =Σ∪D ap ∪D ss ∪D T ∪D R ∪D una ∪D S 0.Five of them (Σ,D ap ,D ss ,D una ,D S 0)are similar to those groups in a BAT in L sc ,and the other two (D T ,D R )are introduced to axiomatize description logic related facts and properties
(see below).However,because L DL sc
allows only two object variables,all axioms must conform to the following additional requirements.
Action precondition axioms D ap :
For each ac-tion A in L DL
sc ,there is one axiom of the form P oss (A,s )≡ΠA [s ](or P oss (A (x ),s )≡ΠA (x )[s ],or P oss (A (x,y ),s )≡ΠA (x,y )[s ],respectively),if A is an action constant (or unary,or binary action term,respectively),where ΠA (or ΠA (x ),or ΠA (x,y ),respectively)is a C 2formula with no free variables (or with at most x ,or with at most x,y as the only free variables,respectively).This set of axioms characterize the preconditions of all actions.
Successor state axioms D ss :There are two types of ?uents in L DL sc :primitive dynamic concepts of the form F (x,s )(?uents with exactly one non-situation argument)and primitive dynamic roles of the form F (x,y,s )(?uents with exactly two non-situation arguments).Let variable vector x to be x ,or y ,or x,y ;a SSA is speci?ed for each ?uent F ( x ,do (a,s )).According to the general syntactic form of the SSAs provided in [Reiter,2001],without loss of generality,we can assume that the axiom has the form
F ( x ,do (a,s ))≡ψF (
x ,a,s ),(1)where the general structure of ψF ( x ,a,s )is as follows:
m 0
i =1[?x ][?y ](a =A +
i ( x (i,0,+))∧φ+i ( x (i,1,+))[s ])∨F ( x ,s )∧?( m 1
j =1[?x ][?y ](a =A ?
j ( x (j,0,?))∧φ?j (
x (j,1,?))[s ])),where each variable vector x (i,n,b )(or x (j,n,b )respectively)
(i =1..m 0,j =1..m 1,n ∈{0,1},b ∈{+,?})represents a vector of object variables,which can be empty,x ,y , x,y or y,x .Moreover,[?x ]or [?y ]represents that the quanti?er
included in []is optional;and each φ+i (
x (i,1,+)),i =1..m 0(φ?i ( x (j,1,?)),j =1..m 1,respectively),is a C 2formula with variables (both free and quanti?ed)among x and y .Note that when m 0(or m 1respectively)is equal to 0,the corresponding disjunctive subformula is equivalent to false .Acyclic TBox axioms D T :Similar to the TBox axioms in DL,we may de?ne new concepts using TBox axioms.Any group of TBox axioms D T may include two sub-classes:static TBox D T,st and dynamic TBox D T,dyn .Every formula in static TBox is a concept de?nition formula of the form
G (x )≡φG (x ),
where G is a unary predicate symbol and φG (x )is a C 2for-mula in the domain with free variable x ,and there is no ?uent in it.Every formula in dynamic TBox is a concept de?nition formula of the form G (x,s )≡φG (x )[s ],
where φG (x )is a C 2
formula with free variable x ,and there is at least one ?uent in it.All the concepts appeared in the left-hand side of TBox axioms are called de?ned concepts.We also require that the set of TBox axioms must be acyclic (acyclicity in D T is de?ned exactly as it is de?ned for TBox ).RBox axioms D R :Similar to the idea of RBox in DL,we may also specify a group of axioms,called RBox axioms be-low,to support a role taxonomy.Each role inclusion axiom is represented as R 1(x,y )[s ]?R 2(x,y )[s ],
where R 1and R 2are primitive roles (either static or dy-namic).If these axioms are included in the BAT D ,then it is assumed that D is speci?ed correctly in the sense that the meaning of any RBox axiom included in the theory is cor-rectly compiled into SSAs.That is,one can prove by induc-tion that (D ?D R )|=?s.R 1(x,y )[s ]?R 2(x,y )[s ].Al-though RBox axioms are not used by the regression operator,they are used for taxonomic reasoning in the initial theory.Initial theory D S 0:It is a ?nite set of C 2sentences (assum-ing that we suppress the only situation term S 0in all ?uents).It speci?es the incomplete information about the initial prob-lem state and also describes all the facts that are not change-able over time in the domain of an application.In particular,it includes static TBox axioms D T,st as well as RBox axioms in the initial situation S 0(if any).In addition,D S 0also in-cludes all unique name axioms for object constants.
The remaining two classes (foundational axioms for situ-ations Σand unique name axioms for actions D una )are the same as those in the BATs of the usual SC.Note that these axioms (as well as D ap and D ss )use more than two variables (e.g.,D ss use action and situation variables in addition to ob-ject variables),but we will see in the next section,that these axioms will be eliminated in the process of regressing a re-gressable formula to a sentence that will use no more than two object variables and no other variables.
4Modi?ed Regression with Lazy Unfolding
After giving the de?nition of what the BAT in L DL sc is,we turn our attention to the reasoning tasks.
Given a formula W of L DL sc in the domain D ,the de?ni-tion of W being regressable (called L DL sc regressable below)is slightly different from the de?nition of W being regress-able in L sc (see [Reiter,2001])by adding the following two conditions:(i)any variable (free or bounded)in W is either x or y ;(ii)every term of sort situation in W is ground.More-over,in L DL sc we have to be more careful with the de?nition of the regression operator R for two main reasons.First,to deal with TBox we have to extend regression.For a L DL sc regress-able formula W ,we extend below the regression operator de-?ned in [Reiter,2001]with the lazy unfolding technique (see [Baader et al.,2003])to expand de?ned dynamic concepts.We still denote such operator as R .Second,L DL sc uses only two object variables and we have to make sure that after re-gressing a ?uent atom we still get a L DL sc formula,i.e.,that we never need to introduce new (free or bound)object vari-ables.To deal with the two-variable restriction,we modify our regression operator R in comparison to the conventional operator de?ned in [Reiter,2001].For example,when replac-ing P oss atom or ?uent atoms about do (α,σ),the de?nition of the conventional regression operator in [Reiter,2001]has the assumption that the quanti?ed variables in the right-hand side of the corresponding axioms should be renamed to new variables different from the free variables in the atoms that to be replaced.This assumption of using new variables for re-naming assures equivalence of original formula and the for-mula after regression.To avoid introducing new variables (as required by the Reiter’s regression operator)and to assure de-?ned dynamic concepts being handled,we modify the regres-sion operator for each L DL sc regressable formula.Possibility of reusing variables is guaranteed by the general format of the SSAs given in the previous section and the additional condi-tion (ii)in the de?nition of the L DL sc regressable formula.The complete formal de?nition of our R is as follows,where σdenotes the term of sort situation,and αdenotes the term of sort action.
?If W is not atomic,i.e.W is of the form W 1∨W 2,W 1∧W 2,?W ,Qv.W where Q represents a quanti?er (in-cluding counting quanti?ers)and v represents a variable sym-bol,then
R [W 1∨W 2]=R [W 1]∨R [W 2],R [?W ]=?R [W ],R [W 1∧W 2]=R [W 1]∧R [W 2],R [Qv.W ]=Qv.R [W ].
?
Otherwise,W is atom.There are several cases.a.If W is of the form A 1( t )=A 2( t )for some action function symbols A 1and A 2,then by using axioms in D una ,2we de?ne the regression of W as
R [W ]= ⊥if A 1=A 2, | t |i =1t i =t
i otherwise .Otherwise,if W is situation independent atom (including
equality between object constants or variables),or W is a concept or role uniform in S 0,then
R [W ]=W.b.
If W is a regressable P oss atom,so it has the form
2
Notice that the action functions with different number of argu-ments always use different function symbols (i.e.,different names).
P oss (A ( t ),σ),for terms of sort action and situation respec-tively in L DL sc .Then there must be an action precondition
axiom for A of the form P oss (A ( x ),s )≡ΠA (
x ,s ),where the argument x of sort object can either be empty (i.e.,A is an action constant),a single variable x or two-variable vector x,y .Because of the syntactic restrictions of L DL sc ,each term in t can only be a variable x ,y or a constant C .Then,
R [W ]=8
>>>><>>>>:R [(?y )(x =y ∧ΠA (x,y,σ))]if t = x,x ,
R [(?x )(y =x ∧ΠA (x,y,σ))]else if t = y,y ,R [ΠA ( t ,σ)]else if t = x,C or t = x,y or t =x,R [f ΠA (
t ,σ)]otherwise,
where C is a constant and φ
denotes a dual formula for formula φobtained by replacing every variable symbol x (free or quanti?ed)with variable symbol y and replacing every variable symbol y (free or quanti?ed)with variable
symbol x in φ,i.e., φ
=φ[x/y,y/x ].c.If W is a de?ned dynamic concept,so it has the form
G (t,σ)for some object term t and situation term σ,and there must be a TBox axiom for G of the form G (x,s )≡φG (x,s ).Because of the restrictions of the language L DL sc ,term t can only be a variable x ,y or a constant.Then,we use lazy unfolding technique as follows:
R [W ]=
j
R [φG (t,σ)]if t is not variable y,
R [f φG (y,σ)]
otherwise .
d.If W is a primitive concept (a primitive role,respectively),so it has the form F (t 1,do (α,σ))or F (t 1,t 2,do (α,σ))for some terms t 1(and t 2)of sort object,term αof sort action and term σof sort situation.There must be a SSA for ?uent F such as Eq.(1).Because of the restriction of the language L DL sc ,the term t 1and t 2can only be a variable x ,y or a constant C and αcan only be an action function with no more than two arguments of sort object.Then,when W is a concept,
R [W ]=
j
R [ψF (t 1,α,σ)]if t 1is not variable y,
R [f ψF (y,α,σ)]
otherwise,i.e.,if t 1=y ;
and,when W is a role,
R [W ]=8
>>><>>>:
R [(?y )(x =y ∧ψF (x,y,α,σ))]if t 1=x,t 2=x ;R [(?x )(y =x ∧ψF (x,y,α,σ))]if t 1=y,t 2=y ;R [f ψF (y,x,α,σ)]if t 1=y,t 2=x ;or t 1=y,t 2=C ;R [ψF (t 1,t 2,α,σ)]
otherwise.
Based on the above de?nition,we are able to prove the following theorems.
Theorem 1Suppose W is a L DL sc regressable formula,then the regression R [W ]de?ned above terminates in a ?nite num-ber of steps.
Proof:Immediately follows from conditions (i )and (ii )of the de?nition of L DL sc regressable formula,acyclicity of the TBox axioms,and from the assumption that RBox axioms are compiled into the SSAs and consequently do not partici-pate in regression.
Theorem 2Suppose W is a L DL
sc regressable formula with the background basic action theory D .Then,R [W ]is a L DL sc formula uniform in S 0with no more than two variables (x
and y ).Moreover,D |=W ≡R [W ],and
D |=W iff D S 0|=R [W ].
Proof:According to the de?nition of the modi?ed regres-sion operator,prove by induction over the structure of W .The ?rst statement holds because all replacements done by R transform W to logically equivalent formula.The sec-ond statement follows from the regression theorem in [Reiter,2001]. Theorem 3Suppose W is a L DL sc regressable formula with the background basic action theory D .Then,the problem whether D |=W is decidable.Proof:According to Theorem 2,D |=W iff D S 0|=R [W ],where R [W ]and the axioms in D S 0are C 2formu-las.Therefore,the problem whether D |=W is equivalent to whether D S 0∧?R [W ]is unsatis?able or not,which is a decidable problem,according to the fact that the satis?ability
problem in C 2is decidable.
This theorem is important because it guarantees that the projection and executability problems in L DL sc are decidable even if the initial KB D S 0is incomplete.[Gu and Soutchan-ski,2006]give some detailed examples that illustrate the ba-sic reasoning tasks described above and reduction techniques for dealing with properties that need more than two variables,and show that using L DL sc ,one can model realistic dynamic domains such as school enrollment services and on-line shop-ping services.
We say that the SSA for a ?uent F is context-free if the SSA for F has the form
F ( x ,do (a,s ))≡γ+F
( x ,a )∨F ( x ,s )∧?γ?F ( x ,a ).Then,we have the following theorem about the complexity analysis for reasoning about projection problem.Theorem 4Given a basic action theory D in L DL sc ,suppose that the SSA for a ?uent F is context-free,then the com-putational complexity of answering the queries of the form
F ( X,
σ)is co -NE XP T IME ,where X is a vector of object constants and σis a ground situation term.
Proof:The result follows from the complexity analysis of projection problem in [Reiter,2001](Chapter 4),Theorem 3,and the theorem in [Pratt-Hartmann,2005]that the satis?a-bility problem in C 2is decidable in NE XP T IME .
5Progression of CNF -based KBs
The progression problem (also known as ?ltering and update)
is how to compute the new theory in response to a given se-quence of actions.In this section,we consider the progres-sion problem for KBs in language L DL sc .In this section,let D =D ss ∪D ap ∪Σ∪D una .
A formal de?nition of (classical)progression is given in [Reiter,2001].A set of sentences D S αis the (classical)pro-gression of the initial K
B D S 0(wrt basic action theory D )af-ter performing a ground action αin the situation S 0iff D S αis uniform in do (α,S 0),D |=D S α,and for every model M αof D ∪D S α,there is a model M of D such that M and M αhave the same domain and interpret situation independent predi-cates,function symbols,P oss and all ?uents about the future of do (α,S 0)identically (in the sequel,we say that M and M α
have a progression relationship ).The progression can be iter-atively repeated if the progressed KB has the same format as
the initial KB and we can consider the computed progression as the new initial KB at the next iteration.[Lin and Reiter,1997]shows that the (classical)progression of a ?nite FO KB is not always FOL de?nable (but it is always de?nable in the second-order logic).By using an example similar to [Lin and Reiter,1997],one can prove
Theorem 5Progression of a theory in L DL sc is not always FO de?nable,therefore it is de?nitely not de?nable in L DL sc .Proof:We consider the theory D 1obtained by modify-ing the theory D given in [Lin and Reiter,1997]as follows:(1)replace one constant symbol 0in D by an in?nite set of constant symbols {0,1,2,···};(2)replace function symbol succ (x )=y in D by predicate succ (x,y )which will be true iff y is the successor of x ;(3)replace the empty initial KB by the new D S 0which includes in?nitely many axioms of the form c 1=c 2for any non-identical constant symbols c 1and c 2given above and of the form succ (c,c )where constant c is the successor of constant c in the sense of natural numbers.The rest of the proof is exactly the same as the proof given in [Lin and Reiter,1997]. Notice that the proof assumes that an L DL sc theory D 1is in?nite.The problem whether progression of a ?nite theory in L DL sc is always FO de?nable remains open.
Now,we consider a (weaker than classical)modi?ed pro-gression for certain type of incomplete KBs only.For this special case of incomplete KBs,we show below that a mod-i?ed progression of a KB is in L DL sc and it is sound wrt a classical progression of this KB.
First,we restrict the syntactic form of the KBs that are al-lowed.We use e to range over ewffs ,that is,quanti?er-free boolean formulas with equalities and inequalities only.For any vector x that is x,y (or a variable x ,or y )and any vec-tor of object constants B
that is B 1,B 2 (or a single constant B ),we write x = B
as an abbreviation for x =B 1∧y =B 2(or x =B ,respectively).We use l ( x ,S )to range over ?uent literals ,where S is a ground situation term.We call formu-las of the form ? x .e ( x )?l ( x ,S )equality-based formulas .We de?ne a CNF-based KB D S =KB I ∪KB S ,where KB I is a set of situation-independent formulas (including unique name axioms for object constants,i.e.,KB I is a subset of D S 0),and KB S is a ?nite set of sentences uniform in S ,where each sentence (also called clause below)is a disjunc-tion of ?nitely many equality-based formulas.In particular,D S 0=KB I ∪KB S 0.A CNF formula composed from ground ?uent literals uniform in S is a simple example of KB S .Secondly,we consider an action theory D that is local-effect .Let a SSA of a ?uent F have the syntactic form
F ( x ,do (a,s ))≡γ+F
( x ,a,s )∨F ( x ,s )∧?γ?F ( x ,a,s ).This SSA is local-effect if γ+F ( x ,a,s )and γ?
F ( x ,a,s )are disjunc-tions of formulas of the form ? z [a =A ( y )∧φ( y ,s )],where A is a action function, y contains x , z = y ? x ,and φis quanti?er-free.An action theory D is local-effect if each SSA in D is local-effect.Let ?be +or ?.Consider a ground ac-tion αand a ?uent F i in a local-effect action theory D of language L DL sc ,then it is easy to see that the right-hand side (RHS)of SSA for F i ( x ,do (α,s ))has the following syntactic
form: m +i k =1( x = B +ik ∧φ+ik (s ))∨F i ( x ,s )∧? m ?
i k =1(
x = B ?ik ∧φ?ik
(s )),where each m ?i is a natural number,the variables in x are among x and y ,and for each k ,φ?ik (s )is a propositional formula.This SSA is a special case of the generic SSA (1)from Section 3.Moreover,according to The-orem 3the problem whether D |=φ?ik (S )is decidable for each k and any ground situation S .We de?ne the following abbreviations.
Add (F i ,α,S )def
=
W
{k ∈1..m +i |D |=φ+ik
(S )} x = B +ik
,Add (?F i ,α,S )def
=
W
{k ∈1..m ?i |D |=φ?ik (S )} x = B ?ik
,Delete (F i ,α,S )def =
_k =1..m ?i
x = B ?ik ∧?_{k |D |=?φ?ik
(S )} x = B ?ik Delete (?F i ,α,S )def
=
_k =1..m +i x = B +ik ∧?
_
{k |D |=?φ+ik
(S )} x = B
+ik When there is no disjunct satisfying the condition on the con-text formula φ?ik ,the corresponding disjunction is equivalent
to ⊥.It is easy to see that all formulas above are ewffs.
The intuition behind these abbreviations is simple.For instance,Add (F i ,α,S )is a collection of all those cases when F i will become true in every model if the context φ+ik (S )holds in S .Therefore,these cases provide support for adding the ?uent F i to the new KB.If one takes all those
cases x = B ?ik
when F i ceases to be true in some models (where contexts might or might not be entailed)and removes from them those cases when negations of contexts are known to be entailed (i.e.,remove models where it is guaranteed that F i will not cease to be true),then as a result one gets Delete (F i ,α,S )that represents the collections of all those objects for which F i has to be deleted from the current KB.Now consider a ground action αand a CNF-based KB D S =KB I ∪KB S as the current KB of a local-effect BAT D =D ∪D S .Assume that D |=P oss (α,S ),otherwise there is no need in progression.We provide an algorithm to com-pute a variant of progression,called a modi?ed progression of D S wrt D and the ground action αexecuted in S ,and denote the resulting KB as P (α,D S ).
Let P (α,D S )be the following set of sentences:
1.Initialize P (α,D S )to KB I ∪
{(? x )Add (F i ,α,S )?F i (
x ,do (α,S ))|Add (F i ,α,S )≡⊥}∪{(? x )Add (?F i ,α,S )??F i ( x ,do (α,S ))|Add (?F i ,α,S )≡⊥}.2.For each clause in KB S of the form C j =p 1∨···∨p h ∨···,
where each p h is an equality-based formula (?
x )e j h ( x )?l j h (
x ,S )and l j h is either F i or its negation ?F i ,we update this clause as follows.
(a)Initialize a temporary set T =?.(b)For each p h ,if
KB I ∪{(?
x )e j h ( x )∧?Delete (l j h ,α,S )}|=⊥,add (? x )e j h (
x )∧?Delete (l j h ,α,S )?l j h ( x ,do (α,S ))into the set T .(c)If T =?,add a new clause C
j
=W p ∈T p to P (α,D S );otherwise,do nothing (i.e.,replace C j with ).
It is easy to see that the resulting KB P (α,D S )remains to
be a CNF-based KB in L DL sc .Therefore,such progression can be repeated for the next ground action,say α .
The intuition behind this algorithm is simple.The succes-
sor model of the KB after performing a ground action at the current situation should keep all the situation-independent in-formation,add truth values for each ?uent for those objects where it will de?nitely become true (or false),and also keep the remaining consistent information by removing con?ict-ing knowledge for objects from the current KB.Note that we detect con?icts between cases supported by e j h and cases included in the Delete (l j h ,α,S )condition by using unique name axioms for constants in KB I ,if necessary,to solve the entailment problem in (b).
For any given BAT D =D ∪D S and a ground action α,we say that a modi?ed progression P (α,D S )is (classically)sound if any model of the classical progression of D S (wrt αand D )is a model of the modi?ed progression.Also,we say that P (α,D S )is (classically)complete if every model of D ∪P (α,D S )is a model of the classical progression of D S (wrt αand D ).The modi?ed progression has the following nice properties.
Theorem 6Given a BAT D with the current KB D S and a ground action αthen
(1)If D is consistent and RHS of SSAs are consistent,then the modi?ed progression P (α,D S )is also consistent.
(2)The modi?ed progression P (α,D S )is (classically)sound.Proof:(1)Prove by cases using the de?nition of P (α,D S ).(2)According to the de?nition of P (α,D S ),prove that D |=
P (α,D S )using the RHS of the SSAs for F i (
x ,do (α,S )).Let M αbe any model of the (classical)progression of D S .Then,there is a model M of D such that M and M αhave a progression relationship.Then M is also a model of P (α,D S )by D |=P (α,D S ),and then since M and M αhave a progression relationship we can prove that M αis a model of any sentence uniform in do (α,S )iff M is a model of any sentence uniform in do (α,S ).Therefore,we conclude that M αis a model of P (α,D S )because P (α,D S )is a set of sentences uniform in do (α,S ).
6Discussion and Future Work
The major consequence of the results proved above for the problem of service composition is the following.If both atomic services and properties of the world that can be af-fected by these services have no more than two parameters,then we are guaranteed that even in the state of incomplete in-formation about the world,one can always determine whether a sequentially composed service is executable and whether this composite service will achieve a desired effect.The previously proposed approaches made different assumptions:[McIlraith and Son,2002]assumes that the complete infor-mation is available about the world when effects of a com-posite service are computed,and [Giacomo et al.,1999]con-siders the propositional fragment of the SC.
As we mentioned in Introduction,[McIlraith and Son,2002]propose to use Golog for composition of Semantic Web services.It is surprisingly straightforward to de?ne al-most all Golog operators starting from our C 2based SC.The only restriction in comparison with the original Golog [Re-iter,2001]is that we cannot de?ne the operator (πx )δ(x ),non-deterministic choice of an action argument,because L DL sc
regressable formulas cannot have occurrences of non-ground
action terms in situation terms.
The recent paper[Baader et al.,2005]proposes integration
of description logics A L CQ IO(and its sub-languages)with
an action formalism for reasoning about Web services.We
discuss that paper in[Gu and Soutchanski,2006].
An interesting paper[Liu and Levesque,2005]aims to
achieve computational tractability of solving projection and
progression problems.The theory of the initial KB is as-
sumed to be in the so-called proper form(i.e.,conjunctions
of equality-based formulas)and the query used in the projec-
tion problem is expected to be in a certain normal form.They
consider a weaker type of progression de?ned for proper KBs
with local effect actions only and show that their progression
is sound(and sometimes complete)wrt the classical progres-
sion.We also consider local effect action theories,but our
CNF-based KB is a set of disjunctions of equality-based for-
mulas.However,[Liu and Levesque,2005]considers a SC
formulated in a general FOL(where the entailment problem
is undecidable)and impose no restrictions on arity of?uents.
Because of these signi?cant differences in our approaches,it
is not possible to compare them.
It is obvious that all cases from[Lin and Reiter,1997;
Shirazi and Amir,2005;Liu and Levesque,2005]when the
progression is FOL de?nable also can be applied to our case
simply because we restrict the language to two object vari-
ables only.However,we do the disjunctive case that nobody
did before.Also,[Liu et al.,2006]considers update of an
ABox in a DL following[Winslett,1990]and also mentions
that update can be applied to a boolean ABox formulated in
C2,but their update is de?ned in terms of a conjunction of primitive?uent literals,i.e.,it is different from our progres-
sion because our update is de?ned in terms of changes in the
theory due to a ground action.[Giacomo et al.,2006]gener-
alized the update approach of[Liu et al.,2006]from A L C to a
more expressive DL language DL-Lite which allows general
inclusion assertions in TBox,showed that the result of an up-
date is always expressible by a DL-Lite ABox and provided
a polynomial-time algorithm that computes the update over a
DL-Lite KB.
The most important direction for future research is ef?cient
implementation of practical scenarios of reasoning in L DL
sc .
Although in general,the worst-case computational complex-
ity for the reasoning problems in L DL
sc is high,some practi-
cal scenarios may facilitate empirically ef?cient solutions to the projection and executability problems.We are planning to consider also the progression problem for a more general class of incomplete KBs and conditions when the modi?ed progressions is(classically)complete. Acknowledgments
Thanks to the Natural Sciences and Engineering Research Council of Canada and to the Department of Computer Sci-ence of the University of Toronto for partial?nancial support. References
[Baader et al.,2003]Franz Baader,Diego Calvanese,Deb-orah McGuinness,Daniele Nardi,and Peter F.Patel-Schneider,editors.The Description Logic Handbook:
Theory,Implementation,and Applications.Cambridge University Press,2003.
[Baader et al.,2005]Franz Baader,Carsten Lutz,Maja Mili?c i′c,Ulrike Sattler,and Frank Wolter.Integrating de-scription logics and action formalisms:First results.In Proc.of AAAI-05,pages572–577,Pittsburgh,USA,July 2005.An extended version:LTCS-Report-05-02from http://lat.inf.tu-dresden.de/research/reports.html. [Borgida,1996]Alexander Borgida.On the relative expres-siveness of description logics and predicate logics.Arti?-cial Intelligence,82(1-2):353–367,1996.
[Giacomo et al.,1999]Giuseppe De Giacomo,Luca Iocchi, Daniele Nardi,and Riccardo Rosati.A theory and im-plementation of cognitive mobile robots.J.of Logic and Computation,9(5):759–785,1999.
[Giacomo et al.,2006]Giuseppe De Giacomo,Maurizio Lenzerini,Antonella Poggi,and Riccardo Posati.On the update of description logic ontologies at the instance level.In Proc.of AAAI-06,pages1271–1276,Boston, MA,USA,July2006.AAAI Press.
[Gu and Soutchanski,2006]Yilan Gu and Mikhail Soutchanski.A logic for decidable reasoning about services.In Proceedings of AAAI-06workshop on AI-Driven Technologies for Services-Oriented Computing, Boston,MA,USA,2006.https://www.doczj.com/doc/fb740370.html,/?yilan/publications/papers/aaai06.pdf.
[Lin and Reiter,1997]F.Lin and R.Reiter.How to progress
a database.Arti?cial Intelligence,92:131–167,1997. [Liu and Levesque,2005]Yongmei Liu and Hector J.
Levesque.Tractable reasoning with incomplete?rst-order knowledge in dynamic systems with context-dependent actions.In Proc.of IJCAI-05,pages522–527,Edinburgh, Scotland,UK,August2005.
[Liu et al.,2006]H.Liu,C.Lutz,https://www.doczj.com/doc/fb740370.html,icic,and F.Wolter.
Updating description logic ABoxes.In Proc.of KR2006, pages46–56,Lake District,UK,June,2-52006. [McIlraith and Son,2002]Sheila McIlraith and Tran Son.
Adapting Golog for composition of semantic web services.
In Proc.of KR2002,pages482–493,Toulouse,2002. [Pacholski et al.,1997]Leszek Pacholski,Wies?aw Szwast, and Lidia https://www.doczj.com/doc/fb740370.html,plexity of two-variable logic with counting.In Proc.of LICS-97,pages318–327,Warsaw, Poland,1997.A journal version:SIAM Journal on Com-puting,v29(4),1999,p.1083–1117.
[Pratt-Hartmann,2005]Ian https://www.doczj.com/doc/fb740370.html,plexity of the two-variable fragment with counting quanti?ers.Jour-nal of Logic,Lang.and Inf.,14(3):369–395,2005. [Reiter,2001]Raymond Reiter.Knowledge in Action:Logi-cal Foundations for Describing and Implementing Dynam-ical Systems.The MIT Press,2001.
[Shirazi and Amir,2005]Afsaneh Shirazi and Eyal Amir.
First-order logical?ltering.In Proc.of IJCAI-05,pages 589–595,Edinburgh,Scotland,UK,2005. [Winslett,1990]Marianne S.Winslett.Updating logical databases.The Academic Press,1990.
1.《水晶》（新人对唱的） 2.《真想见到你》（李汶的歌，新娘独唱的哦，实力派！） 3.《月亮代表我的心》（比较悠久啦） 4.《深情相拥》（对新人的唱功要求颇高啊） 5.《很爱很爱你》（也是新娘独唱哦，不过改了歌词，例如”看着她走向你，那幅画面多美丽”改成“我现在走向你，那幅画面多美丽”） 6.《第一次》（光良的歌，不用我多说了吧） 7.《love,love,love》（八错，调动现场气氛满灵的，新娘唱的也八错滴好象唱歌的新娘居多，我们的男士们很害羞呢） 8.《明明很爱你》（马来西亚的歌手唱的歌满受JMS的欢迎，大概是曲风比较明快吧） 9.《神话》（成龙大哥的版本比较通俗，八过对MM的要求高些，韩红的版本实力派的JMS挑战一下啊！） 10.《选择》（内敛型的JMS可以考虑的一种） 11.《最浪漫的事》（经典的歌曲，用在婚礼上再合适不过。） 12.《宁静的夏天》（节奏轻快，简洁，个人满喜欢，夏天结婚的可以试试） 13.《牵手》（应该是满老的歌了，有空我去听下再发表意见恩，听了个开头就知道了，应该是满苦情的歌，婚礼上就需要考虑是否适合了额．跟年龄有关吧） 14.《你最珍贵》（又一个对唱功有要求的） 15.《恋爱达人》（利用歌词可以搞些小剧情，效果应该不错。） 16.《恋爱频率》（看来是对流行音乐把握很敏锐的MM，） 17.《我只在乎你》（大家帮忙改改歌词吧） 18.《明明白白我的心》（简单的情歌，不太唱歌的JMS也可以小试身手了） 19.《你是我最深爱的人》（应该是男士发挥的时候了吧） 20.《屋顶》（个人还是喜欢杰伦的版本） 21.《在我生命中的每一天》（对唱的、抒情的慢歌永远是大家的最爱+首选） 22.《小夫妻》（一般用来做背景音乐较多的歌，可能太通俗了些，唱的人八多啊，不过还 是赞一个） 23.《不得不爱》（） 24.《爱你一万年》（LG唱给LP听，记住表情,一定要深情!迷倒一大片。。。。。掌声鼓励一下） 25.《让我取暖》（很适合年轻夫妻对唱的情歌，有Young的气息） 26.《明天我要嫁给你了》 27.《你是我的老婆》（好歌啊，好歌。。。，终于又有适合GG们独唱的好歌了。） 28.《大城小爱》（） 29.《你是我的幸福吗》（MM们独唱之作，不要害羞，大胆的唱给GG们听吧！） 30.《出嫁》（zhangning_she MM真是需要再表扬一下，提供了这么多歌，而且首首都这么经典，不错的情歌，可对唱） 31.《我愿意》（可独唱，也可双人合唱的佳作） 32.《你是我心底的烙印》（一人一句，配合默契啊） 33.《甜蜜蜜》（邓JJ的怀旧老歌，永远最好听） 34.《北极雪》（旋律很容易上口，不只冬天适合唱，夏天唱可以带来一丝凉意） 35.《被风吹过的夏天》（如果是在夏天相恋的JMS注意了额，这里就有一首适合你们对唱 的歌曲了）
2012年高考湖北卷 家有名士 1 南朝2 刘义庆 3 ?王湛4 既除所生服5 ，遂停墓所6 。兄王浑7 之子济 8 每来拜墓9，略不过叔10，叔亦不候。济脱时过11，止 12 寒温13而已。后聊14试问近事15，答对甚有音辞16，出 济意外，济极惋愕17。仍与语，转造18清微19 。济先略无20子侄之敬21，既闻其言，不觉懔然22，心形23俱肃24。 遂留共语，弥日累夜25。济虽俊爽26，自视缺然27 ，乃喟然28 叹曰：“家有名士，三十年而不知！” ?济去，叔送至门。济从骑1 有一马，绝．2 难乘，少3 能骑者。济聊4问叔：“好5骑乘不？”曰：“亦好尔。”济 又使骑难乘马，叔姿形6既妙，回策如萦7，名骑8无以 9 过之。济益10叹其11难测，非复12 一事。 ?【邓粲1 《晋纪》曰：“王湛字处冲，太原人。隐德，人莫之知，虽兄弟宗族，亦以为痴，唯父昶异焉。昶丧，居 墓次2，兄子济往省3湛，见床头有《周易》4 ，谓湛曰：‘叔 父用此何为？颇5曾看不？’湛笑曰：‘体中6 不佳时，脱 复看耳7。今日当与汝言。’因8 共谈《易》，剖析入微，济 所未闻，叹不能测9 。 ?济性好马，而所乘马骏驶1 ，意甚爱之。湛曰：‘此虽小驶2，然力薄不堪3 苦。近见督邮马，当胜此，但养不至 耳。’济取督邮马，谷食4 十数日，与湛试之。湛未尝乘马，卒5然便驰骋，步骤不异于济，而马不相胜6 。湛曰：‘今直 行车路7，何以别马胜不8？唯当就．9蚁封10 耳。’于是就蚁封盘马11，果倒踣12，其俊识13天才14乃尔15。”】 ?既还，浑问济：“何以暂行累日1 ？”济曰：“始2 得 一叔。”浑问其故，济具3叹述4如此。浑曰：“何如5 我？”济曰：“济以上人。”武帝每见济，辄以湛调之，曰：“卿家痴叔死未？”济常无以答。既而得叔，后武帝又问如前，济 曰：“臣叔不痴。”称其实美6。帝曰：“谁比7 ？”济曰：“山涛8以下，魏舒9以上。”【《晋阳秋》曰：“济有人伦鉴识10， 见湛，叹服其德宇11 。时人谓湛上方山涛不足，下比魏舒有余。”】 【注】正文选自南朝刘义庆的《世说新语》，【】内的文字是南朝刘孝标的注解。有删改。 ①【名士míng shì】：（1）指已出名而未出仕的人。郑玄注：“名 士，不仕者。”（2）泛指有名的人。杜甫《陪李北海宴历下亭》诗：“海 内此亭古，济南名士多。”（3）特指恃才放达、不拘小节的人。”清 袁赋诚《睢阳尚书袁氏家谱》：“袁可立爱书，不事生产。所与游皆名士”（4）指刑名之士（崇尚法家之士）。《史记·律书》：“自是以后，名士迭兴，晋用咎犯，而齐用王子，吴用孙武，申明军约，赏罚必信。” 【名士】一词，源于我国古代魏晋时期 。魏晋多名士 ，他们的特点： 多隐居，峨冠博带，说怪话但博学多才，形貌潇洒，偶尔也有放浪形骸的。有云：从来圣贤皆寂寞，是真名士自风流 ②【南朝】：南朝（420—公元589，共170年）是东晋之后建 立于南方的四个朝代（宋、齐、梁、陈）的简称。自公元420年刘裕灭亡东晋王朝建立宋，接着是齐、梁、陈，而陈朝最终于589年被隋灭。 它们存在的时间都相对较短，南朝宋（420年—479年，共60年）；南朝齐（479年—502年，共24年）；南朝梁（502年—557年，共56年）；南朝陈（557年—589年，共33年）；其中最长的不过60年，最短的仅有24年，是我国历史上朝代更迭较快的一段时间。此时，中国正处于南北分治的时期，在我国历史上南朝与北方政权北魏、东魏、西魏、北齐、北周并称南北朝。 秦汉三国两晋南北朝隋唐五代十国宋元明清 ③【刘义庆】（403—444），字季伯，汉族，原籍南朝宋彭城（今 江苏徐州）人，文学家，南朝刘宋文学家。刘宋武帝刘裕之侄，在诸王 中颇为出色，十分被看重。刘义庆是这本书的编者，并不为作者。《世说新语》是魏晋南北朝时期“志人小说”的代表作。依内容可分为“德行”“言语”“政事”“文学”“方正”等三十六类，每类收有 若干则，全书共一千多则，每则文字长短不一，有的数行，有的三言两语，从此可见笔记小说“随手而记”的诉求及特性。《世说新语》主要记述世人的生活和思想，及统治阶级的情况，反映了魏晋时期文人想言行，和上层社会的生活面貌，记载颇为丰富真实，描述了当时士人所处的时代状况及政治社会环境，展示了“魏晋清谈”的风貌。京尹时期（15-30岁）。刘义庆15岁一路来平步青云，其中任秘书监一职，掌管国家的图书著作，有机会接触与博览皇家典籍，对《世说新语》的编撰奠定了良好的基础，17岁升任尚书左仆射（相当于副宰相），可惜的是，《世说新语》一书刚刚撰成，刘义庆就因病离开扬州，回到京城不久便英年早逝，时年仅41岁，宋文帝哀痛不已，赠其谥号为“康王”。 ④【王湛zhàn 】：（249～295年），字处冲，西晋太原晋阳（今山 西太原）人，官至西晋汝南内史，又称王汝南，王昶之子，王浑之弟，儿子是王承。少有识度，身长七尺八寸，龙额大鼻，少言语。服完父丧后，闭门不交宾客，冲素简淡，沉静和顺。晚成，被同族认为痴，起初只有父亲王昶欣赏他。后来被侄子王济称赏，在应答晋武帝时说王湛人材在“山涛以下，魏舒以上”，由此渐而知名。二十八岁方出仕，历任秦王文学、太子洗马、尚书郎、太子中庶子、汝南内史。元康五年（295年）去世，时为四十七岁。 【湛zhàn 】1、深：精～。～恩（深恩）。～蓝。湛深 深湛；精深 湛深的艺术功力。2. 清澈：清～。澄～。1.湛蓝 zhànlán 晴天的蓝色；湖海等的深蓝色。.湛清 清澈 天空湛清如水。 【冲素chōn ɡ sù】 亦作“冲素”。冲淡纯朴。 【冲淡chōng dàn 】冲和、淡泊，叫做冲淡。 冲淡和纤秾不同。纤秾用的是浓彩，冲淡施的是淡墨。 冲淡并非淡而无味，而是冲而不薄，淡而有味。 魏晋文人濯足清流，不染尘俗，同封建权贵不合作的精神，对安静、美好的理想境界的憧憬，是形成冲淡的一个重要原因。 ⑤【除所生服】：为父母守丧完毕。 【所生suǒ shēng 】： 1.生 身父母。： 注：“所生，指亲母。” 南朝 宋 刘义庆 《世说新语·赏誉》：“ 王汝南既除所生服，遂停墓所。 【除服】：亦称“除丧”、“脱服”。除去、脱去丧服。谓守孝三年完毕。 ⑥【墓所】：1.墓地，坟地、墓次。 【墓 mù】 埋葬死人的地方：墓穴。墓地。墓园。墓道。墓碑。坟墓。墓志铭。 【所 suǒ】 处，地方：住所。哨所。场所。处所。 机关或其他办事的地方的名称：研究所。派出所。 ⑦【王浑】（223－297），字玄冲，太原晋阳（今山西太原）人。三国曹魏后期至西晋初期的大臣，东汉代郡太守王泽之孙，曹魏司空王昶之子。承袭父亲京陵侯之位，属魏大将军曹爽部下。嘉平元年（249），曹爽被杀，王浑随之免职。后来又被起用为怀县（今河南沁阳）县令，参司马昭的安东将军军事，任散骑黄门侍郎、散骑常侍。咸熙年间（264－265），为越骑校尉。王浑曾辅佐晋武帝和晋惠帝两代君主，在晋初的军事和政治上作出了一定贡献。特别是在平吴作战方面功绩显著，因此官职累累升迁。 ⑧【王济】（246～291），字武子，太原晋阳（今山西太原）人，名士。西晋大将军王浑的次子。王济才华横溢，风姿英爽，气盖一时，被晋武帝司马炎选为女婿，配常山公主。王济爱好弓马，勇力超人，又善《易经》、《老子》、《庄子》等。文词俊茂，名于当世，与姐夫和峤及裴楷齐名。王济年四十六岁，先其父王浑而亡，追赠骠骑将军。 ⑨【拜墓】：拜扫坟墓。拜扫baì sǎo ：在墓前祭奠；扫墓。《南史·梁 纪中·武帝下》：“拜扫山陵，涕泪所洒，松草变色。” 白雪遗音·马头调·雷峰塔》：“清明拜扫，搭船借伞，前世恩人来相见。”⑨【】又如：略等（大约相等，差不多）；略绰（阔大；大略）；略订（约略计算）；略约（约略） ⑩【略不过叔】：基本上、几乎不拜访他的叔叔。 略lüè本义: 封疆土地；天子经略土地,定城国,制诸侯。——《左传·昭公七年》1、基本上，几乎，稍稍，全，皆，都 敬亭丧失其资略尽。—— 清· 黄宗羲《柳敬亭传》 略无慕艳意。——明· 宋濂《送东阳马生序》2 稍稍，稍微；略懂一点，略识文字（初识文字，认字不多）3通“掠”。抢劫;夺取 “属盗起于境，资产略尽，迫寒馁而无忧叹。”---《郝逢传》4、谋略：móu lüè，雄才大略： xióng cái dà lüè：非常杰出的才智和谋略。才，才能。略，计谋。 ?【脱时tuō】：结合上下文，应做有时、偶尔的意思来讲。偏义副词，重点由“时”字联想。脱字确实不知道作什么讲。 脱tuō 肉去骨曰脱。——《尔雅》 1. 离开，落掉：～产。～发（fà）。～节。～离。～落。～贫（摆脱贫困）。～稿（完成著作）。～手。摆～。挣～。临阵逃～。 2. 遗漏：～漏。～误。～文（因抄刊古书而误脱的字。亦称“夺文”）。3. 取下，除去：～下。～帽。～氧。～脂。～胎换骨。4. 倘若，或许：～有不测。5. 轻慢：～略（放任，不拘束）。～易（轻率，不讲究礼貌）。轻～（轻率，不持重，放荡）。 脱产学习就是参加工作后再去校内进行全日制学习的方式，其管理模式与普通高校一样，学习期间不在原单位工作，不占用周六和周日的工休时间，对学生有正常的、相对固定的授课教室和管理要求，有稳定的寒暑假期安排。 ?【止zh ǐ 】： 1. 仅，只：～有此数。不～一回。2. 停住不动：～ 步。截～。3. 拦阻，使停住：～痛。禁～。4. 古同“趾”，脚；脚趾头。 ? 【寒温hán wēn 】 1、.指问候冷暖起居。 晋 干宝 《搜神记》 卷十六：“忽有客通名诣 瞻 ，寒温毕，聊谈名理。” 元 尚仲贤 《柳毅传书》第三折：“施礼罢，叙寒温。”《红楼梦》第一○五回：“众亲友也有认得 赵堂官 的，见他仰着脸不大理人，只拉着 贾政 的手笑着説了几句寒温的话。” 管桦《将军河》第一部第四一章：“﹝ 董士清 ﹞不自然地呲着牙，满口寒温：‘诸位冷不冷啊？辛苦啦！’”2、冷暖。宋 司马光 《和始平公见寄》诗：“违离詎几时，风色变寒温。”3.中医指两种药性，寒性或温性。 明 李时珍 《本草纲目·序例·神农本经名例》：“药有酸、咸、甘、苦、辛五味，又有寒、热、温、凉四气。”注引 宗奭 曰：“寒、热、温、凉，是药之性。” 鲁迅 《二心集·“好政府主义”》：“因为自三民主义以至无政府主义，无论它性质的寒温如何，所开的究竟还是药名。” ?【聊liáo 】本义:耳鸣 1. 姑且，勉强，凑凑和和：～且（姑且）。～ 以自娱。～复尔尔（姑且如此）。～备一格。2. 依赖，寄托：无～。百 无～赖。3. 略微：～表寸心。4. 闲谈：～天。闲～。5. 耳鸣：～啾。 ?【近事】：近日之事，过去不久的事情。 ?【音辞yīn cí】 1.言谈；辞令。 南朝 宋 刘义庆 《世说新语?赏誉》：“后聊试问近事，答对甚有音辞，出 济 （ 王济 ）意外。” 北齐 颜之推 《颜氏家训?勉学》：“以外率多田野閒人，音辞鄙陋，风操蚩拙。”2.文词。 唐 刘知几 《史通?序例》：“ 枚乘 首唱《七发》，加以《七章》、《七辩》，音辞虽异，旨趣皆同。”3.音调歌词。《旧唐书?曹确传》：“ 可及 善音律，尤能转喉为新声，音辞曲折惋愕，听者忘倦。”惋愕 ?【惋愕wǎn è】：怅叹惊愕《梁书·昭明太子统传》：“太子仁德 素著，及薨，朝野惋愕。” 【 惋w ǎn 】： 叹惜，憾恨：～惜。～伤。～叹。悲～。哀～。【愕è】：1. 惊讶：～胎。～异。惊～。错～。闻之～然。 ?【造zào 】：1、到。造访；夜造(深夜前往造访);造府拜瞻(敬辞。 到府上去拜访);造请(前往问候、拜见);造谒(造请);造谢(登门致谢) 2、[学 业等]达到的程度或境界。在本文引申为转至、转到。⒉（学业或技艺）所达到的程度：造～。苦心孤～（指刻苦钻研，达到别人不及的境地）。【造诣zào yì】（1）学业、学问等修炼的成果。如：造诣很深。（2）拜访。《晋书·陶潜传》：“酣醉便反，未尝有所造诣。”（3）泛指足迹所至。 《新唐书·崔咸传》：“咸素有高世志，造诣崭远，闲游终南山，乘月吟啸，至感慨泣下。”【诣yì】 1.到，旧时特指到尊长那里去：～阙。～前请教。 ?【清微qīng wēi 】 1.清淡微妙。明 贾仲名 《金安寿》第一折： “韵清微，高山流水野猿嘶， 楚 雨 湘 云塞雁飞，清风明月孤鹤唳。” 清 恽敬 《＜靖节集＞书后二》：“其诗清微通澈，雄厉奋发，如其人，如其人焉。” ?【略无）lüè wú】：全无，毫无。《三国志·蜀志·赵云传》“以 云 为翊军将军” 裴松之 注引《赵云别传》：“ 赵云 身自断后，军资什物，略无所弃。”张真 《谈京剧＜猎虎记＞》：“革命，对每个人都是很大的冒险，而这一些人，却都挺身而出，略无难色。”【略lüè】本义:封疆土地；天子经略土地,定城国,制诸侯。——《左传·昭公七年1、基本上，几乎，稍稍，全，皆，都 敬亭丧失其资略尽。—— 清· 黄宗羲《柳敬亭传》 略无慕艳意。——明· 宋濂《送东阳马生序》 ○ 21【敬】：1、尊敬、恭敬。尊重，有礼貌地对待：尊～。致～。～重（zhòng ）。～爱。～仰。恭～。～辞。～慕。～献。2、有礼貌地送 上去：～酒。～香。 ○ 22【懔然lǐn rán 】1.危惧貌；戒惧貌。《荀子·议兵》：“ 紂 刳 比干 ，囚 箕子 ，为炮烙刑；杀戮无时，臣下懍然。” 杨倞 注：“懍然，悚栗之貌。”2.严正貌。 南朝 宋 刘义庆 《世说新语·轻诋》：“ 桓公 懍然作色……四坐既骇，袁亦失色。”杨沫 《青春之歌》第一部第四章：“她咬着嘴唇，懔然地瞪视着这些人。”【懔l ǐn 】◎懔,敬也。——《广雅》，也作 畏惧。懔惧(畏惧);懔畏(畏惧) ○ 23【心形xīn xíng 】： 内心和形体，精神与身体。 南朝 宋 刘义庆 《世说新语·赏誉》：“﹝ 王济 ﹞既闻其言，不觉懔然，心形俱肃。” 唐 白居易 《足疾》诗：“应须学取陶彭泽 ，但委心形任去留。” ○ 24【肃sù】1. 恭敬：～立。～坐。～然。2. 严正，认真：严～。～静。～穆。整～。3. 躬身作揖，迎揖引进：～客。4. 萎缩：～杀。 ○ 25【弥日累夜mí rì lěi yè】 连日连夜，夜以继日。同“夜以继日”。【弥日mí rì】 终日，满日。《后汉书·文苑传下·边让》：“登 瑶臺 以回望兮，冀弥日而消忧。” 李贤 注：“弥，终也。” 南朝 宋 刘义庆 《世说新语·文学》：“ 张 遂诣 刘 …… 真长 延之上坐，清言弥日，因留宿至晓。”清 无名氏 《后会仙记》：“会既散， 仇生 惘然若有所失，悵念弥日。”【弥mí 】 1. 满，遍：～满。～月（ａ．整一个月；ｂ．婴儿满月）。～望（满眼）。～天（满天，形容极大的）。2. 补，合：～补。～缝。～封。3. 更加：～坚。欲盖～彰。4. 水满的样子：～漫。 5. 久，远：～留（病久留不去，后称病重将死）。～亘（连绵不断）。 【累夜lěi yè】连夜。《晋书·荀晞传》：“终日累夜，不出户庭。”唐 杜甫 《奉赠卢五丈参谋》诗：“説诗能累夜，醉酒或连朝。【累léi 】1. 〔～～〕a.连续成串，如“果实～～”；b.颓丧的样子，如“～～若丧家之犬”。2. 〔～赘〕a.多余，不简洁，如“文字～～”；b.使人感到多余或麻烦的事物，如“负重登高，不胜～～”（“赘”均读轻声）。【累lěi 】 ㄌㄟˇ1. 连续，重叠，堆积：～计。～日。～积。～～。日积月～。连篇～牍。2. 照原数目多少而递增：～进税。 3. 连及，连带：～及。牵～。拖～。” ○ 26【俊爽 jùnshuǎng 】英俊豪爽;人品高超,性格豪爽。风姿俊爽；少而俊爽。1、英俊清朗。《晋书·裴楷传》：“ 楷 风神高迈，容仪俊爽。”《旧唐书·裴度传》：“ 度状貌不踰中人，而风彩俊爽。” 茅盾 《动摇》：“但此时眉尖稍稍挑起，却又是俊爽英勇的气概。” 2、雄健敏捷。 元 辛文房 《唐才子传·耿湋》：“诗文俊爽。” ○ 27【缺然quē rán 】1).有所不足。《庄子·逍遥游》：“吾自视缺然，请致天下。” 成玄英 疏：“自视缺然不足，请将帝位让与贤人。” 唐 司空图《与李生论诗书》：“愚幼常自负，既久而逾觉缺然。” 宋 王安石 《除参知政事谢表》：“承弼之任，贤智所难；顾惟缺然，何以堪此？” 清 方苞 《汉文帝论》：“世徒见其奉身之俭，接下之恭，临民之简，以为 黄 老 之学则然，不知正自视缺然之心之所发耳。” (2).缺失。《晋书·张骏传》：“每患忠言不献，面从背违，吾政教
关于函数y=f(x)的理解与分析 作者：周勇 （湖南省长沙市第七中学 邮编：410003） 抽象函数y=f(x)是指没有给出函数的具体解析式，只给出了一些体现函数特征的式子的一类函数。由于抽象函数表现形式的抽象性，使得这类问题成为函数内容的难点之一.抽象性较强，灵活性大,解抽象函数重要的一点要抓住函数中的某些性质，通过局部性质或图象的局部特征，利用常规数学思想方法（如化归法、数形结合法等），这样就能突破“抽象”带来的困难，做到胸有成竹.另外还要通过对题目的特征进行观察、分析、类比和联想，寻找具体的函数模型，再由具体函数模型的图象和性质来指导我们解决抽象函数问题的方法。一般以中学阶段所学的基本函数为背景，构思新颖，条件隐蔽，技巧性强。解法灵活，因此它对发展同学们的 抽象思维，培养同学们的创新思想有着重要的作用。 一、关于定义域的理解与分析 例1. 已知函数)(2x f 的定义域是［1，2］，求f （x ）的定义域。 解：)(2x f 的定义域是［1，2］，是指21≤≤x ，所以)(2x f 中的2x 满足412≤≤x 从而函数f （x ）的定义域是［1，4］ 原理：一般地，已知函数))((x f ?的定义域是A ，求f （x ）的定义域问题，相当于已知 ))((x f ?中x 的取值范围为A ，据此求)(x ?的值域问题。已知f(x)的定义域是A ，求()() x f ?的定义域问题，相当于解内函数()x ?的不等式问题。 又如：已知函数f(x)的定义域是[]2,1- ，求函数()? ?? ? ??-x f 3log 21 的定义域。 再如：定义在(]8,3上的函数f(x)的值域为[]2,2-，若它的反函数为f -1 (x)，则y=f -1 (2-3x)的 定义域为 ，值域为 。(]8,3,34,0?? ??? ? 原理：这类问题的一般形式是：已知函数f （x ）的定义域是A ，求函数))((x f ?的定义域。正确理解函数符号及其定义域的含义是求解此类问题的关键。这类问题实质上相当于已知 )(x ?的值域B ，且A B ?，
因很多家长向麦麦粥铺反映，想要儿歌50首大全的歌词。我们也花了大量的时间和精力，通过手打不断把歌词完善到趋于完整。希望可以让妈妈们和孩子一起在听的同时，更增加一份教学的乐趣。 您的五分好评是我们进步的最大动力，谢谢。 精心整理，真心希望对孩子的培养能有一丝帮助。 【儿歌串烧50首】第1首：《家庭称呼》歌词 爸爸爸爸daddy daddy daddy daddy 妈妈妈妈mami mami mami mami 哥哥弟弟brother brother brother 姐姐妹妹sister sister sister 爷爷爷爷grandpa grandpa grandpa 奶奶奶奶grandma grandma grandma 伯伯叔叔和舅舅 英文全都叫uncle uncle uncle uncle 姑姑婶婶和阿姨 英文全都叫auntie auntie auntie auntie 爸爸爸爸daddy daddy daddy daddy 妈妈妈妈mami mami mami mami 哥哥弟弟brother brother brother 姐姐妹妹sister sister sister 爷爷爷爷grandpa grandpa grandpa 奶奶奶奶grandma grandma grandma 伯伯叔叔和舅舅 英文全都叫uncle uncle uncle uncle 姑姑婶婶和阿姨 英文全都叫auntie auntie auntie auntie 爸爸爸爸daddy daddy daddy daddy 妈妈妈妈mami mami mami mami 哥哥弟弟brother brother brother 姐姐妹妹sister sister sister 爷爷爷爷grandpa grandpa grandpa 奶奶奶奶grandma grandma grandma 伯伯叔叔和舅舅 英文全都叫uncle uncle uncle uncle 姑姑婶婶和阿姨 英文全都叫auntie auntie auntie auntie 【儿歌串烧50首】第2首：《家族歌》歌词 爸爸的爸爸叫什么？爸爸的爸爸叫爷爷； 爸爸的妈妈叫什么？爸爸的妈妈叫奶奶； 爸爸的哥哥叫什么？爸爸的哥哥叫伯伯； 爸爸的弟弟叫什么？爸爸的弟弟叫叔叔； 爸爸的姐妹叫什么？爸爸的姐妹叫姑姑。 妈妈的爸爸叫什么？妈妈的爸爸叫外公； 妈妈的妈妈叫什么？妈妈的妈妈叫外婆；
本站歌词来自互联网北极雪下在那头 寂寞不寂寞 谁的想念是他的等候你若问我快不快乐寂寞不寂寞 牵你手贴我手 感觉我的脉搏 你要试着了解 试着体会 用心好好感觉 然后你才能够看得见快乐伤悲 也许我的眼泪 我的笑脸 只是完美的表演 听说北极下了雪 北极雪下在那头 寂寞不寂寞 谁的想念是他的等候你若问我快不快乐寂寞不寂寞 牵你手贴我手 感觉我的脉搏 你要试着了解 试着体会 用心好好感觉 然后你才能够看得见快乐伤悲 也许我的眼泪 我的笑脸 只是完美的表演 听说北极下了雪 你要试着了解 试着体会 用心好好感觉 然后你才能够看得见快乐伤悲 也许我的眼泪 我的笑脸 只是完美的表演 听说北极下了雪 你要试着了解 试着体会
用心好好感觉 然后你才能够看得见 快乐伤悲 也许我的眼泪 我的笑脸 只是完美的表演 听说北极下了雪 本站歌词来自互联网 本站歌词来自互联网 想唱就唱 演唱:张含韵 推开夜的天窗 对流星说愿望 给我一双翅膀 能够接近太阳 我学着一个人成长 爱给我能量 梦想是神奇的营养 催促我开放 想唱就唱 要唱的响亮 就算没有人为我鼓掌 至少我还能够勇敢的自我欣赏想唱就唱 要唱的漂亮 就算这舞台多空旷 总有一天能看到挥舞的荧光棒想唱就唱 演唱:张含韵 推开夜的天窗 对流星说愿望 给我一双翅膀 能够接近太阳 我学着一个人成长 爱给我能量 梦想是神奇的营养 催促我开放 想唱就唱 要唱的响亮 就算没有人为我鼓掌 至少我还能够勇敢的自我欣赏想唱就唱 要唱的漂亮 就算这舞台多空旷
总有一天能看到挥舞的荧光棒想唱就唱 要唱的响亮 至少我还能够勇敢的自我欣赏就算没有人为我鼓掌 想唱就唱 要唱的漂亮 就算这舞台多空旷 总有一天能看到挥舞的荧光棒想唱就唱 本站歌词来自互联网 本站歌词来自互联网 弦子- 沿海地带 空荡荡的月台 入秋微凉的海 微风把脚下的树叶都吹开 火车就要出发催促我快离开 我的心已超载 你不了解的爱 当失望逐渐将一切都掩埋 没想到害怕更真实存在 在沿海地带放逐我的爱 孤单也很精采 我相信我们都有该去的未来 不该在原地徘徊 MUSIC 我其实很明白 梦醒了就不在 只是还挣扎着不让他离开 紧紧抓着的也都是空白 在沿海地带放逐我的爱 孤单也很精采 我相信我们都有该去的未来 不该在原地徘徊 在沿海地带我远远离开 要更自由自在 不要我的心随着大厅的钟摆 停留在原地感慨 本站歌词来自互联网
10 味道 作词：姚谦 作曲：黄国伦 演唱：张学友 专辑：张学友活出生命Live演唱会 今天晚上的星星很少 不知道它们跑那去了 赤裸裸的天空 星星多寂廖 我以为伤心可以很少 我以为我能过的很好 谁知道一想你 思念苦无药 无处可逃 想念你的笑 想念你的外套 想念你白色袜子 和你身上的味道 我想念你的吻和手指淡淡烟草味道 记忆中曾被爱的味道
今天晚上心事很少 不知道这样算好不好 赤裸裸的寂寞 朝着心头绕 我以为伤心可以很少 我以为我能过的很好 谁知道一想你 思念苦无药 无处可逃 想念你的笑 想念你的外套 想念你白色袜子 和你身上的味道 我想念你的吻和手指淡淡烟草味道 记忆中曾被爱的味道 想念你的笑 想念你的外套 想念你白色袜子 和你身上的味道 我想念你的吻和手指淡淡烟草味道 记忆中曾被爱的味道 这首歌是张学友活出生命Live演唱会上翻唱辛晓琪的。辛晓琪这首歌是1994年出来的，在上高中时，早晨广播中有时候就会播放这首歌。听到辛晓琪的“味道”，还真没有什么味道，总觉得她的声音不对，总觉得有点像一个怨妇在回忆。如果这首歌让张惠妹，或者声音不那么尖的人唱会更好一点。而张学友版的“味道”，真的唱出了“味道”的“味道”。一种成熟的人，面对自己的过去，面对自己空荡荡的内心。这是一种理性的回味，是一种让人怜爱的心痛。能让人听出她的不舍，听出她内心的伤痛。所以，这个男版的味道才真正的唱出了这首歌的意境和胸襟。 这首歌也是年纪稍微大一点的人所喜欢的歌曲。所以，在这里解析，也算是比较有代表性，代表了70后的人对情感的回味。 其实听这首歌就可以感受到很重的70后气息。这么投入的女人，想念外套，问题是还想念袜子。我觉得我们八零，九零的，那有空去想起来谁的白色袜子啊。但是，这样的风格适合九十年代初的风格，那时候，流行音乐还是比较新鲜的东西，人们抒情也比较委婉。这样的歌曲在当时已经是很够意思了。 另外一点，我要补充的是，我保证，就在今天之前，我还不知道是谁作的词，就刚才才查的，又是姚谦。他在那个时候已经如此牛了。这首歌已经传唱
红歌100首（歌词大全） 1.十送红军 (合)一送里格红军 介支个下了山 秋风里格细雨.. 介支个缠绵绵.. 山上里格野鹿 声声哀号 树树里个梧桐 叶呀叶落光 问一声亲人红军啊.. 几时里格人马 介支个再回山 (男)三送里格红军 介支个拿那山.. 山上里格包谷.. 介支个金灿灿 包谷种子 介支个红军种 包谷棒棒咱们就能掰.. 紧紧拉着红军手 红军啊 撒下的种子 介支个红了天 (女)五送里格红军 介支个过了坡 鸿雁里格阵阵 介支个空中过 鸿雁里格能够 捎书信 鸿雁里格飞到天涯海角千言万语嘱咐 红军啊 捎信里格多保.. 介支格革命说 (女)七送里格红军 介支个五斗江 江上里格船儿 介支个穿梭忙 千军万马 介支个江畔站 十万百姓泪汪汪思情似海不能忘 红军啊 革命成功 介支个早回乡 (男)九送红军上大道 锣儿无声鼓不敲000 鼓不敲 双双里格拉着长茧的手 心像里格黄莲脸在笑 血肉之情怎能忘 红军啊 盼望里个早日.. 介支个传捷报 (合)十送里格红军 介支个望月亭 望月里格边上 介支个搭高台 高台里格十丈 白玉柱 雕龙里格画凤 放呀放光彩 朝也盼来晚也想 红军啊 这台里格名叫.. 介支个望红台 2.红军战士想念毛主席 抬头望见北斗星 心中想念毛泽东 想念毛泽东 迷路时想你有方向 黑夜里想你照路程 黑夜里想你照路程 湘江岸你燃起火炬冲天 亮 号召工农闹革命 井岗山你率领我们打天 下 红旗一展满地红 抬头望见指路星 心中想念毛泽东 想念毛泽东 困难时想你有力量 胜利时想你心里明 胜利时想你心里明 瑞金城你首创革命根据 地 工农掌权好威风 赣江边你率领我们反围 剿 杀败蒋匪百万兵 啊... 红军是你亲手创 战略是你亲手定 革命战士怀念你 伟大的领袖毛泽东 革命战士怀念你 伟大的领袖毛泽东 3.红星歌 红星闪闪放光彩 红星灿灿暖胸怀 红星是咱工农的心 党的光辉照万代 红星是咱工农的心 党的光辉照万代 长夜里红星闪闪驱黑暗 寒冬里红星闪闪迎春来 斗争中红星闪闪指方向 征途上红星闪闪把路开 红星闪闪放光彩 红星灿灿暖胸怀 跟着毛主席跟着党 闪闪的红星传万代 跟着毛主席跟着党 闪闪的红星传万代 4.映山红 夜半三更哟盼天明 寒冬腊月哟盼春风 若要盼得哟红军来 岭上开遍哟映山红 若要盼得哟红军来 岭上开遍哟映山红 岭上开遍哟映山红 岭上开遍哟映山红 夜半三更哟盼天明 寒冬腊月哟盼春风 若要盼得哟红军来 岭上开遍哟映山红 若要盼得哟红军来 岭上开遍哟映山红 岭上开遍哟映山红 若要盼得哟红军来 岭上开遍哟映山红 岭上开遍哟映山红 岭上开遍哟映山红 5.情深谊长 五彩云霞空中飘 天上飞来金丝鸟 五彩云霞空中飘 天上飞来金丝鸟 诶-…诶-… 红军是咱们的亲兄弟 长征不怕路途遥 诶-…诶-… 索玛花儿一朵朵 红军从咱家乡过 红军走的是革命的路 革命的花儿开在咱心窝 五彩云霞空中飘 天上飞来金丝鸟 诶-…诶-… 红军走的是革命的路 革命的花儿开在咱心窝 1 / 18
每天爱你多一些 也曾追求也曾失落 不再有梦是你为我 推开天窗打开心锁 让希望又转动 忙碌奔波偶而迷惑 为了什么是你给我 一份感动一个理由 不疲倦不脆弱 这世界的永恒不多 让我们也成为一种 情深如海不移如山 用一生爱不完 我的爱一天比一天更热烈 要给你多些再多些不停歇 让你的生命只有甜和美OH OH 遗忘该怎么流浪 我的爱一天比一天更热烈（还要坚决） 要给你多些再多些不停歇（然后再多一些） 让恋人钟爱的每一句誓言OH OH 不再难追全都实现 MUSIC ... 心中有爱人生如歌 唱着欢乐海阔天空 来去从容不惹烦忧 有了你别无求 这世界的永恒不多 让我们也成为一种 情深如海不移如山 用一生爱不完 我的爱一天比一天更热烈 要给你多些再多些不停歇 让你的生命只有甜和美OH OH 遗忘该怎么流浪 我的爱一天比一天更热烈（还要坚决） 要给你多些再多些不停歇（然后再多一些） 让恋人钟爱的每一句誓言OH OH 不再难追全都实现 我的爱一天比一天更热烈 要给你多些再多些不停歇 让你的生命只有甜和美OH OH
遗忘该怎么流浪 我的爱一天比一天更热烈（还要坚决） 要给你多些再多些不停歇（然后再多一些）让恋人钟爱的每一句誓言OH OH 不再难追全都实现 你最珍贵 明年这个时间约在这个地点 记得带着玫瑰打上领带系上思念 动情时刻最美真心的给也不累 太多的爱怕醉 没人疼爱再美的人也会憔悴 我会送你红色玫瑰(你知道我爱流泪) 你别拿一生眼泪相对 未来的日子有你才美梦才会真一点 我学着在你爱里沉醉(我不撤退) 你守护着我穿过黑夜 我愿意这条情路相守相随你最珍贵 动情时刻最美真心的给也不累 太多的爱怕醉 没人疼爱再美的人也会憔悴 我会送你红色玫瑰(你知道我爱流泪) 你别拿一生眼泪相对 未来的日子有你才美梦才会真一点 我学着在你爱里沉醉(我不撤退) 你守护着我穿过黑夜 我愿意这条情路相守相随你最珍贵 我会送你红色玫瑰(你知道我爱流泪) 你别拿一生眼泪相对 未来的日子有你才美梦才会真一点 我学着在你爱里沉醉(我不撤退) 你守护着我穿过黑夜 我愿意这条情路相守相随你最珍贵
剖析函数y=f(x)与y=f[t(x)]的奇偶性 函数的奇偶性是高中数学的重要内容，它与函数的单调性，周期性一起构成研究函数性质的三把钥匙。函数的奇偶性是教学过程中的一个难点，笔者现就教学过程中遇到的问题加以探讨。 教材中奇偶性的定义：一般地，如果对于函数f(x)的定义域内的任意一个x，都有f(-x)=-f(x)则称f(x)为这一定义域内的奇函数。一般地，如果对于函数f(x)的定义域内的任意一个x，都有f(-x)=f(x)则称f(x)为这一定义域内的偶函数。 在函数的奇偶性定义中，若函数y=f（x）的定义域I是关于原点对称（即x?I，则-x?I）且f(-x)=f(x)（或f(-x)=-f(x)）则函数叫偶（或奇）函数。由此可知：函数的定义域关于原点对称是该函数为奇（或偶）函数的必要条件。本文主要谈谈函数y=f（x）与函数y=f(kx+b)(k10)在奇偶性方面的不同表现形式。 例1： y=f(x)是单调递增的奇函数，它的定义域为[-1，1]，求已知函数 1 y. 2 y=f(x) 的定义域为[-1,1] 解：Q 1 x-? \ -1￡231 -1￡x+1￡1 f(23 x-)3-f(x+1) y=f(x)是奇函数 Q 1 \ 2￡2x￡4 -2￡x￡0 x-)3f(-x-1) f(23 y=f(x)是单调递增函数 Q 1 \ -2￡x￡ 23 x-3-x-1
\ -2￡x ￡x ￡-2 或 x 3 1 \x ?{}2- 故2y 的定义域为x ?{}2- 此时2y =0 \ 值域: 2y ?{}0 点评：y=f(x)(x ?R)为奇函数Tf(-x-1)=-f(x+1) (x ?R) 例2： 若函数y=f(2x+1)为奇函数，则f(-2x+1)=___________ 若函数y=f(2x+1)为偶函数，则f(-2x+1)=_____________ 解：由于对应法则后边不是x ，而换成了2x+1,学生无从下手，其实，此题是把自变量x 换成了2x+1后的函数，在运算后的自变量仍然是x ，f(2x+1)是奇函数实质上还是对x 而言的。故y=f(2x+1)是奇函数\f(-2x+1)=-f(2x+1) 同理：若函数y=f(2x+1)为偶函数\ f(-2x+1)=f(2x+1) 点评：若函数y=f(2x+1)为偶函数\ f(-2x+1)=f(2x+1)，即 f(1+2x)=f(1-2x)，这表明函数y=f(a+x) 的图象与y=f(a-x)的图象关于y 轴对称。应注意：y=f(a+x) 的图象与y=f(a-x)的图象关于y 轴对称，这里是两个函数图象间的对称;而函数y=f(a+x)为偶函数，它的图象关于y 轴对称,这里是一个函数图象内部之间的自身的对称。 例3： （2003年安徽三市联考）已知f(2x+1)为偶函数，那么函数f(2x)图像的对称轴方程为_____________ 解法1： Q y=f(2x+1)=f[2(x+12)]的图像向右平移12 个单位得到函数y=f[2(x)]=f(2x)的图像, Q y=f(2x+1)是偶函数\它的图像关于y 轴对称， 即x=0是函数f(2x+1)的图象的对称轴，直线x=0也向右平移12 个单位得直线方程为x=12，故直线x=12 是函数f(2x)的图象的对称轴。 解法2： Q f(2x+1)为偶函数\y=f(-2x+1)=f(2x+1),即f(1-2x)=f(1+2x), Q 定义在R 上的函数y=f(x)满足f(a+x)=f(a-x) (x ?R)，则函数y=f(x)的图象关于直线x=a 对称 \函数y=f(x)的对称轴方程为x=1,故函数y=f(2x)的对称轴方程为x=12 . 点评：y=f(2x+1)为偶函数Tf(-2x+1)=f(2x+1).
一首好歌不仅能够带动KTV的气氛，说不定还能撮合几对哦~~~几百首KTV里面热门的男女对唱，好听，好唱！麦霸们请收藏! 1.《你是我心中的一首歌》王力宏selina 2.《明明很爱你》品冠梁静茹——这个歌曲好听就不说了，主要是MV很有意思，泼一身水，一巴掌，蛮搞笑的，给人感觉也是超级甜蜜的~~ 3,《好心分手》王力宏卢巧音——这歌是粤语的，所以我们唱起来有些费劲，还有一个陆毅和卢巧音的版本《至少走的比你早》，貌似是这个名字，国语的，比较好唱 4《珊瑚海》周杰伦Lara——我心情不好的时候一定会去听这个歌曲 5,《独唱情歌》Tank Selina——个人比较喜欢TANK的创作风格，很不错，很好听的歌曲~~ 6,《美丽的神话》孙楠韩红——这个歌曲是我不敢听得歌曲之一，很多回忆，尤其是成龙和金喜善的版本《神话》，听了很伤感~~ 7,《只对你有感觉》Hebe 飞轮海 8,《Way Back Into Love 》Huge Grant Haley Bennett——很有feeling的一个歌曲，品冠和梁静茹有翻唱过~~梁静茹和品冠也唱过中文版《K歌情人》~~ 9,《水晶》任贤齐徐怀钰——很早的歌曲，记忆犹新的歌词“我和你的爱情，好像水晶......”是叫人感觉爱情甜蜜的歌曲~~ 点击播放 10,《梁山伯与茱丽叶》卓文萱曹格——本来是两对情侣中各自的男女主人公，被安在一个歌曲里面，歌曲很经典~~ 11,《北极雪》陈慧琳冯德伦——此歌曲还有一个新版本，是小刚和陈慧琳的《再见北极雪》 12,《选择》叶倩文林子祥——这个歌曲我印象不深，不过歌曲应该很老，很经典~~ 13,《让梦冬眠》孙楠艾雨——很考验的一个歌曲，主要是男高音太高
民间小调歌词 1、十二月调情（歌词） （男唱）正月里调情正月正，我看到二小妹子俊俏又年轻，皮白肉又嫩呐，我的妹子呀，玩耍没关门，乖乖，你爱坏多少人。 （女唱）二小妹子听此言慌忙开言道，叫一声情郎哥哥听奴细根苗，大街上走一趟啊我的哥哥，小郎子长的标哎呀爱坏了奴家了。 （男唱）二月里调情龙抬头，我看到二小妹子站在大门口，打你家门前过呀我的妹子啊，两眼不睬我乖乖真叫我心难过。 （女唱）二小妹子听此言慌忙开言道，叫一声情郎哥哥听奴细根苗，不是不睬你呀，我的哥哥，大街上人太多哎呀看到了笑话我。 （男唱）三月里调情桃花杏花开，我看见二小妹子站在大门外，东张又西望啊，我的妹子啊，问你看哪个乖乖你实话跟我讲。 （女唱）二小妹子听此言慌忙开言道，叫一声情郎哥哥听奴细根苗，隔壁有个王大妈我的哥哥她会拉马扯皮条，一拉就成了。 （男唱）四月里调情大麦小麦黄，我给我的二小妹子买布做
衣裳，青纱、哔叽尼啊，我的妹子啊，两样要哪样妹子你快快跟我讲。 （女唱）二小妹子听此言慌忙开言道，叫一声情郎哥哥听奴细根苗，两样我都不要我的哥哥，只要你心肠好哎呀你常常来跑跑。 （男唱）五月里调情是端阳，我看见二小妹子站在大门旁，不高又不矮啊，我的妹子啊，不瘦又不胖乖乖谁也比不上。（女唱）二小妹子听此言慌忙开言道，叫一声情郎哥哥听奴细根苗，俺人才又不标啊，我的哥哥啊，奴人丑心肠好哎呀金钱也比不了。 （男唱）：六月里调情三伏天，我看见二小妹子有点心想变，隔壁有个王老板啊，我的妹子呀，常往你家跑，乖乖你想把我抛。 （女唱）二小妹子听此言慌忙开言道，叫一声情郎哥哥听奴细根苗，哪有这件事啊，我的哥哥呀，我可对天表，变心雷打天火烧。 （男唱）七月里调情秋风凉，我看到二小妹子脸色又发黄，你得的什么病呀？我的妹子，快快你跟我将乖乖拿药去熬汤。 （女唱）二小妹子听此言慌忙开言道，叫一声情郎哥哥听奴细根苗，茶饭不想吃，我的哥哥夜晚睡不着哎呀这日子真难熬。
120首KTV里面热门的男女对唱（麦霸们请收藏！） 一首好歌不仅能够带动KTV的气氛，说不定还能撮合几对哦~~~120首KTV里面热门的男女对唱，好听，好唱！麦霸们请收藏! 1.《你是我心中的一首歌》王力宏 selina 2.《明明很爱你》品冠梁静茹——这个歌曲好听就不说了，主要是MV很有意思，泼一身水，一巴掌，蛮搞笑的，给人感觉也是超级甜蜜的~~ 3,《好心分手》王力宏卢巧音——这歌是粤语的，所以我们唱起来有些费劲，还有一个陆毅和卢巧音的版本《至少走的比你早》，貌似是这个名字，国语的，比较好唱~~ 4《珊瑚海》周杰伦 Lara——我心情不好的时候一定会去听这个歌曲 5,《独唱情歌》Tank Selina——个人比较喜欢TANK的创作风格，很不错，很好听的歌曲~~ 6,《美丽的神话》孙楠韩红——这个歌曲是我不敢听得歌曲之一，很多回忆，尤其是成龙和金喜善的版本《神话》，听了很伤感~~ 7,《只对你有感觉》Hebe 飞轮海 8,《Way Back Into Love 》Huge Grant Haley Bennett——很有feeling的一个歌曲，品冠和梁静茹有翻唱过~~梁静茹和品冠也唱过中文版《K歌情人》~~ 9,《水晶》任贤齐徐怀钰——很早的歌曲，记忆犹新的歌词“我和你的爱情，好像水晶......”是叫人感觉爱情甜蜜的歌曲~~ 点击播放 10,《梁山伯与茱丽叶》卓文萱曹格——本来是两对情侣中各自的男女主人公，被安在一个歌曲里面，歌曲很经典~~ 11,《北极雪》陈慧琳冯德伦——此歌曲还有一个新版本，是小刚和陈慧琳的《再见北极雪》 12,《选择》叶倩文林子祥——这个歌曲我印象不深，不过歌曲应该很老，很经典~~ 13,《让梦冬眠》孙楠艾雨——很考验的一个歌曲，主要是男高音太高 14,《You make me wanna》萧亚轩 Blue——因为这个歌曲还有一场官司，不过我本人比较喜欢这首歌曲，就是rap，比较费劲~~ 15,《千里之外》周杰伦费玉清——我们同学两个人，唱的很像原声，我也听过演唱会JAY的独唱，不过好像少了费先生少了点味道~~
怎样求y=Asin(ωx+?)的解析式 学习了正弦函数y=Asin(ωx+?)(A>0，ω>0)后，经常会遇到确定其解析式的问题。这里振幅A 常由函数的最值确定，ω则由周期公式T=2π ω 来求得，问题的关键是求初相?。本文介绍确定正弦函数解析式的两种基本方法。 一、待定系数法 分析正弦曲线y=Asin(ωx+?)(A>0，ω>0)满足的几何条件，列出关于A 、ω、?的三个方程，从而解出A 、ω、?，这就是待定系数法。 例1 若函数y=Asin(ωx+?)(A>0，ω>0，00，ω>0)的图象如图1所示，求此函数的解析式。 分析：由图1提供的信息，正弦曲线相邻的最大、最小值之间为周期的 12 。 ∴ 2T =56π－6π=23 π，即T=43π，∴ω=2T π=32 又显然有A=2，下面只须求初相?。 设曲线与x 轴交C ，易知，C(2π,0)将A=2，ω=32，x=2 π ， y=0代入y=Asin(ωx+?)得0=2sin(34 π +?)。 ∴?=k π－34 π ，(k ∈Z)。注意到y=Asin(ωx+?)的图象是由y=sinx 的图象，经过振幅、周 期变换，且向右平移而得，当k=0时，?在区间[－π,π]上有解。∴?=－34 π ，故函数的 解析式是y=2sin(32x －34 π )。 二、平移变换 我们知道，设A>0，ω>0，正弦函数y=Asin(ωx+?)=Asin[ω(x+? ω)] 的图象，可以看成是由函数y=sinx 的图象经过下面变换而得到： y=sinx 的图象 →y=Asinx 图1