A Predicate Connection Graph Based Logic With Flexible Control

LaTeX实战经验：如何写算法LaTeX中实现的呈现主要有两种⽅式：使⽤宏包algorithm2e, 这个宏包有很多可选项进⾏设定。

使⽤宏包algorithm与algorithmic,使⽤宏包algorithm2e：\usepackage[linesnumbered,boxed,ruled,commentsnumbered]{algorithm2e}%%算法包，注意设置所需可选项例⼦:\IncMargin{1em} % 使得⾏号不向外突出\begin{algorithm}\SetAlgoNoLine % 不要算法中的竖线\SetKwInOut{Input}{\textbf{输⼊}}\SetKwInOut{Output}{\textbf{输出}} % 替换关键词\Input{\\The observed user-item pair set $S$\;\\The feature matrix of items $F$\;\\The content features entities $A := \{A^u,A^v\}$\;\\}\Output{\\$\Theta \ := \{Y^u,Y^v\}$\;\\$W := \{W^u,W^v\}$\;\\}\BlankLineinitialize the model parameter $\Theta$ and $W$ with uniform $\left(-\sqrt{6}/{k},\sqrt{6}/{k}\right)$\; % 分号 \; 区分⼀⾏结束 standarized $\Theta$\;Initialize the popularity of categories $\rho$ randomly\;\Repeat{\text{convergence}}{Draw a triple $\left(m,i,j\right)$ with 算法\ref{al2}\;\For {each latent vector $\theta \in \Theta$}{$\theta \leftarrow \theta - \eta\frac{\partial L}{\partial \theta}$}\For {each $W^e \in W$}{Update $W^e$ with the rule defined in Eq.\ref{equ:W}\;}}\caption{Learning paramters for BPR\label{al3}}\end{algorithm}\DecMargin{1em}使⽤宏包algorithm与algorithmic\usepackage{algorithm, algorithmic}\begin{algorithm}\renewcommand{\algorithmicrequire}{\textbf{Input:}}\renewcommand{\algorithmicensure}{\textbf{Output:}}\caption{Bayesian Personalized Ranking Based Latent Feature Embedding Model}\label{alg:1}\begin{algorithmic}[1]\REQUIRE latent dimension $K$, $G$, target predicate $p$\ENSURE $U^{p}$, $V^{p}$, $b^{p}$\STATE Given target predicate $p$ and entire knowledge graph $G$, construct its bipartite subgraph, $G_{p}$\STATE $m$ = number of subject entities in $G_{p}$\STATE $n$ = number of object entities in $G_{p}$\STATE Generate a set of training samples $D_{p} = \{(s_p, o^{+}_{p}, o^{-}_{p})\}$ using uniform sampling technique \STATE Initialize $U^{p}$ as size $m \times K$ matrix with $0$ mean and standard deviation $0.1$\STATE Initialize $V^{p}$ as size $n \times K$ matrix with $0$ mean and stardard deviation $0.1$\STATE Initialize $b^{p}$ as size $n \times 1$ column vector with $0$ mean and stardard deviation $0.1$\FORALL{$(s_p, o^{+}_{p}, o^{-}_{p}) \in D_{p}$}\STATE Update $U_{s}^{p}$ based on Equation~\ref{eq:sgd1}\STATE Update $V_{o^{+}}^{p}$ based on Equation~\ref{eq:sgd2}\STATE Update $V_{o^{-}}^{p}$ based on Equation~\ref{eq:sgd3}\STATE Update $b_{o^{+}}^{p}$ based on Equation~\ref{eq:sgd4}\STATE Update $b_{o^{-}}^{p}$ based on Equation~\ref{eq:sgd5}\ENDFOR\STATE \textbf{return} $U^{p}$, $V^{p}$, $b^{p}$\end{algorithmic}\end{algorithm}重新定义require和ensure命令对应的关键字(此处将默认的Require/Ensure⾃定义为Input/Output)\renewcommand{\algorithmicrequire}{\textbf{Input:}}\renewcommand{\algorithmicensure}{\textbf{Output:}}。

Temporal RDFClaudio Gutierrez1,Carlos Hurtado1,and Alejandro Vaisman21Department of Computer ScienceUniversidad de Chile{cgutierr,churtado}@dcc.uchile.cl2Department of Computer ScienceUniversidad de Buenos Airesavaisman@dc.uba.arAbstract.The Resource Description Framework(RDF)is a metadatamodel and language recommended by the W3C.This paper presents aframework to incorporate temporal reasoning into RDF,yielding tem-poral RDF graphs.We present a semantics for temporal RDF graphs,asyntax to incorporate temporality into standard RDF graphs,an infer-ence system for temporal RDF graphs,complexity bounds showing thatentailment in temporal RDF graphs does not yield extra asymptoticcomplexity with respect to standard RDF graphs and sketch a temporalquery language for RDF.1IntroductionThe Resource Description Framework(RDF)[14]is a metadata model and lan-guage recommended by the W3C for building an infrastructure of machine-readable semantics for the data on the Web,a long-term vision known as Se-mantic Web.In the RDF model,the universe to be modeled is a set of resources, essentially anything that can have a universal resource identifier,URI.The lan-guage to describe them is a set of properties,technically binary predicates.De-scriptions are statements very much in the subject-predicate-object structure. Both subject and object can be anonymous objects,known as blank nodes.In addition,the RDF specification includes a built-in vocabulary with a norma-tive semantics(RDFS)[4].This vocabulary deals with inheritance of classes and properties,as well as typing,among other features allowing the descriptions of concepts and relationships that can exist for a community of people and software agents,enabling knowledge sharing and reuse.Although some studies exist about addressing changes in an ontology[15],or the need for temporal annotations on Web documents[22],little attention has deserved the problem of representing,updating and querying temporal informa-tion in RDF.Time is present in almost any Web application.Indeed,as pointed out by Abiteboul[1]the modeling of time is one of the key primitives needed in a query language for Web and semistructured data.Thus,there is a clear need of applying temporal database concepts to RDF to allow metadata navigation across time.Fig.1.Initial RDF graph(left)and after some changes(right).Consider an RDF graph describing information about a university,as of its creation time,Figure1(left).Students were classified as technical,graduate or undergraduate,and the only graduate programs offered were at the level of ‘Master’studies,like MBA or MSc;‘Professional Diploma’was the only program offered at the technical level.As the university evolved,a Ph.D program was created.Figure1(right)illustrates the new situation.Notice the dynamics of this example:students(e.g.,John)can enroll in one program(e.g.,Undergraduate), then shift to another one(e.g.,Master),and so on.Thefigures show that the impact of disregarding the time dimension is twofold:on the one hand,when a change occurs,a new metadata document must be created(and the current document dropped).On the other hand,queries asking for past states of the metadata cannot be supported.For instance,we cannot ask for the programs offered at the time when the university was created.1.1Problem Statement:Introducing Time into RDFGenerally speaking,a temporal database is a repository of temporal information. Although temporal databases were initially studied for adding the time dimen-sion to relational databases,as new data models emerged,temporal extensions to these models were also proposed(see Section1.2).We next discuss the main issues that arise when extending RDF with temporal information.Versioning vs.Time Labeling There are two mechanisms for adding the time dimension to non-temporal RDF graphs:labeling and versioning(following the timestamp and snapshot models,respectively).The former consists in labeling the elements subject to changes(i.e.triples).The latter is based on maintaining a snapshot of each state of the graph.For instance,each time a triple changes,a new version of the RDF graph is created,and the past state is stored somewhere. Although both models are equivalent,versioning appears to be not suitable for queries of the form:“all time instants whereΦholds in the database”.There are at least two temporal dimensions to consider when dealing with temporal databases:valid and transaction times.Valid time is the time when data is valid is the modeled world;transaction time is the time when data is actually stored in the database.The versioning approach captures transaction time,while labeling is mostly used when representing valid time.The approach we present in this paper supports both time dimensions.Fig.2.A temporal RDF graph accounting for the evolution of the university ontology.In summary,we believe that for RDF data,labeling is better than versioning, because(a)it preserves the spirit of the distributed and extensible nature of RDF,and(b)in scenarios where changes are frequent and only affecting a few elements of the document,creating a new physical version of the graph each time an update occurs may lead to large overheads when processing temporal queries that span multiple versions.Time Points vs.Time Intervals We will work with the point-based temporal domain for defining our data model and query language,but we will encode time-points in intervals when possible,for the sake of clarity.We will consider time as a discrete,linearly ordered domain,as usual in virtually all temporal database applications.An ordered pair[a,b]of time points,with a≤b,denotes the closed interval from a to b.Figure2shows a temporal RDF graph for the university example above.The arcs in the graph are labeled with their interval of validity.3 For example,the interval[0,Now]says that the triple(technical,sc,student)is valid from the document’s creation time to the current time.Also,note that the figure shows that John was an Undergraduate student in the interval[0,10],and now he is a PhD student.Vocabulary for Temporal Labeling Temporal labeling can be implemented within the RDF specification,making use of a simple additional vocabulary,as Figure3 shows.As we adopted the point-based,discrete and linearly ordered temporal domain,the left and right hand sides of Figure3are equivalent.We will use both representations indistinctly.Moreover,we define constructs that allow moving between intervals and time instants as follows:the instants depicted in Figure3 (left)can be encoded in an interval as shown in Figure3(right).Both alternatives will be used in the query language.3Note that the standard graph(ical)representation of an RDF graph is not the most faithful to convey the idea of statements(triples)being labeled by a temporal ele-ment.Technically,temporal labels should be attached to a whole subgraph u p→v, and not only to an arc.aFig.3.Point-based labeling(left)and Interval-based labeling(right). Temporal Entailment An RDF graph can be regarded as a knowledge base from which new knowledge,i.e.,other graphs,may be entailed.Entailment in a tem-poral setting is a slightly more involved in the RDF case than in the standard database case.In principle,one may be tempted to define the semantics as in temporal relational databases,i.e.,defining the temporal database as the union of all of its snapshots.(A snapshot at time t of a temporal RDF graph G is the corresponding subgraph formed by triples labeled by and instant t.)Blank nodes impose some constraints to this naive approach.For example,each of the three snapshots of Figure4(right)entails the corresponding snapshots of Figure4 (left).However,the whole graph of Figure4(left)cannot be entailed by the graph of Figure4(right).Indeed,the graph of Figure4(left)states that there is an anonymous object X in the triple(a,b,X)at times3and4,which is not the case for the other graph.Temporal Query Language Regarding query languages in temporal databases, basically two choices for defining the temporal domains exist:the point-based and the interval based temporal domains,yielding different query languages[20, 3].In the point-based approach,temporal variables in query languages refer to individual time instants,while in the interval-based domain,variables in the queries range over intervals,making queries more complicated and unnatural. Anyway,one can move easily between these two domains.1.2Related WorkThe RDF model was introducedfive years ago as a W3C recommendation[14]. Formal work in RDF includes the study of formal aspects of RDF data and query languages[10,21],considering RDF features like the entailment,presence of blank nodes,reification,premises in queries,and the RDFS vocabulary with predefined semantics.Several languages for querying RDF data have been pro-posed and implemented.Some of them in the lines of traditional database query languages(e.g.SQL,OQL),others based on logic and rule languages.Good sur-veys are[13,16].To the best of our knowledge,there is still no formal study of temporality issues in RDF graphs and RDF query languages.Temporal database management has been extensively studied,including data models,mostly based on the relational model and query languages[19],leading to the TSQL2language[18].Beyond the relational model,managing historicalFig.4.Temporal entailment:for each t the corresponding snapshots at t are equivalent, but the graph on the left is not entailed by the graph on the right. semistructured data wasfirst proposed by Chawathe et al[6],who extended the Object Exchange Model(OEM)with the ability to represent updates and to keep track of them by means of“deltas.”Later,Dyreson et al[7]allowed anno-tations on the edges of the database graph.In the XML world,Amagasa et al[2] introduced a temporal data model based on XPath for thefirst time.Dyreson[8] proposed an extension of XPath with support for transaction time by means of the addition of several temporal axes for specifying temporal directions,focus-ing on document versioning over the web in the absence of explicit time stamps. Chien et al[5]proposed update and versioning schemes for XML through an edit-based schema in which the most current version of the document is main-tained,and reverse edit scripts allow moving backward in time.Gao et al[9] introducedτXQuery,an extension to XQuery supporting valid time while main-taining the data model unchanged.Mendelzon et al[17]proposed a temporal model for XML,a temporal extension to XPath,and a novel indexing strategy for temporal XML documents.Like in our approach,they use labeling,and a point-based temporal domain and query language.Finally,Visser et al[22]pro-posed a temporal reasoning framework for the Semantic Web,which has been applied in BUSTER,an ontology-based prototype developed at the University of Bremen,supporting the so-called concept@location in time type of query.1.3ContributionsIn this paper we present a framework to incorporate temporal reasoning into RDF,yielding temporal RDF graphs.In particular,we present the following con-tributions:(a)a semantics for temporal RDF graphs in terms of the semantics of non-temporal RDF and RDFS graphs;(b)a study of properties of temporal RDF graphs and the interplay between timestamp and snapshot semantics in temporal RDF graphs;(c)a syntax to incorporate this framework into standard RDF graphs,which includes a vocabulary and rules.The syntax uses the stan-dard RDF vocabulary plus temporal labels;(d)a sound and complete inference system for temporal RDF graphs;(e)complexity bounds which show that entail-ment in temporal RDF graphs does not yield extra asymptotic time complexity with respect to standard RDF graphs;(f)a sketch for a temporal query language for RDF.For the sake of space,we do not include proofs in this version of the paper.2RDF PreliminariesIn this section we present a streamlined formalization of the RDF model following the W3C documents[14,12,4],along the lines of[10].2.1RDF Graphs.Assume there is an infinite set U(RDF URI references);an infinite set B= {N j:j∈N}(Blank nodes);and an infinite set L(RDF literals).A triple (v1,v2,v3)∈(U∪B)×U×(U∪B∪L)is called an RDF triple.In such a triple, v1is called the subject,v2the predicate and v3the object.We often denote by UBL the union of the sets U,B and L.An RDF graph(just graph from now on)is a set of RDF triples.A subgraph is a subset of a graph.The universe of a graph G,universe(G),is the set of elements of UBL that occur in the triples of G.The vocabulary of G is the set universe(G)∩(U∪L).We will use letters N,X,Y,...to denote blank nodes,and a,b,c,... for URIs and literals.A graph is ground if it has no blank nodes.Graphically we represent RDF graphs as follows:each triple(a,b,c)is represented by the labeled graph a b→c.Note that the set of arc labels can have non-empty intersection with the set of node labels.A map is a functionµ:UBL→UBL preserving URIs and literals,i.e.,µ(u)=u andµ(l)=l for all u∈U and l∈L.Given a graph G,we define µ(G)as the set of all(µ(s),µ(p),µ(o))such that(s,p,o)∈G.A mapµis consistent with G ifµ(G)is an RDF graph,i.e.,if s is the subject of a triple, thenµ(s)∈UB,and if p is the predicate of a triple,thenµ(p)∈U.In this case, we say that the graphµ(G)is an instance of the graph G.An instance of G is proper ifµ(G)has fewer blank nodes than G.This means that eitherµsends a blank node to an URI or a literal,or identifies two blank nodes of G.We will overload the meaning of map and speak of a mapµ:G1→G2if there is a map µsuch thatµ(G1)is a subgraph of G2.Two graphs G1,G2are isomorphic,denoted G1∼=G2,if there are maps µ1,µ2such thatµ1(G1)=G2andµ2(G2)=G1.We define two operations on graphs.The union of G1,G2,denoted G1∪G2, is the set theoretical union of their sets of triples.The merge of G1,G2,denoted G1+G2,is the union G1∪G 2,where G 2is an isomorphic copy of G2whose set of blank nodes is disjoint with that of G1.Note that G1+G2is unique up to isomorphism.2.2RDFS VocabularyThere is a set of reserved words defined in the RDF vocabulary description language,RDF Schema[4],–just rdfs-vocabulary for us–that may be used to de-scribe properties like attributes of resources(traditional attribute-value pairs),and also to represent relationships between resources.It defines classes and prop-erties that may be used for describing groups of related resources and relation-ships between resources.4Classes are sets of resources.Elements of a class are known as instances of that class.To state that a resource is an instance of a class, the property rdf:type may be used.The following are the most important classes (in brackets the name we will use in this paper)rdfs:Resource[res],rdfs:Class [class],rdfs:Literal[literal],rdfs:Datatype[datatype],rdf:XMLLiteral[xmlLit], rdf:Property[property].Properties are binary relations between subject re-sources and object resources.The built-in properties are:rdfs:range[range], rdfs:domain[dom],rdf:type[type],rdfs:subClassOf[sc],rdfs:subPropertyOf[sp].3Temporal RDF GraphsIn this paper we extend RDF graphs by allowing temporal elements to label triples.A temporal label is a temporal element t labeling a triple(a,b,c).For simplicity,without loss of generality,we will work with single intervals insteadof temporal elements.In an RDF graph,given a triple(a,b,c),the temporal element t represents the time period when the triple was valid,i.e.the valid time of the triple.At this time we do not deal with transaction time,which can be addressed in an analogous way.3.1Basic DefinitionsIn this section we define the notion of temporal RDF at a conceptual level.Definition1(Temporal graph).1.A temporal triple is an RDF triple with a temporal label(a natural number).We will use the notation(a,b,c):[t].The expression(a,b,c):[t1,t2]is a notation for{(a,b,c):[t]|t1≤t≤t2}.2.A temporal graph is a set of temporal triples.A subgraph is a subset of thegraph.For a temporal graph G,define the snapshot at time t as the RDF graphG(t)={(a,b,c)|(a,b,c):[t]∈G}The underlying RDF graph of a temporal RDF graph G,denoted u(G),istG(t),the union of the graphs G(t).For an RDF graph,define G t as the temporalization of all its triples by a temporal mark t,that is,G t={(a,b,c):[t]|(a,b,c)∈G}.4We omit in this paper vocabulary intended to describe lists,collections,some varia-tions on these,as well as vocabulary to help document and describe other function-alities for which there is no normative semantics.The complete vocabulary can be consulted in[4].The above definitions give the following elementary consequences about the relationship between RDF graphs and temporal RDF graphs.Lemma 1.Let G be an RDF graph,and G be a temporalRDF graph.Then:(1)G t (t )=G ;(2)(G (t ))t ⊆G ,and (3)G = t (G (t ))t .Several issues on the definition of temporal RDF graph are in order:–Recall we use a temporal model where an interval [a,b ]is of the form [a,a +1,...,b ]for a given unit of time that we will assume to be universal in this paper.The natural way to approach this issue is to specify,together with the temporal mark,the unit of time it represents.All the results given here extend without difficulties to this setting.–Temporal triples do not belong to the RDF syntax.In the next section we introduce an RDF-complying syntax for temporal triples,using a small temporal vocabulary.–Source of a temporal statement:Due to the extensible nature of the RDF model,it is possible to include the source of a temporal statement (i.e.who is the author of the temporal statement),and other properties that apply.Although our model (see next section)allows this,we will not study the semantic consequences of this extra information in this paper,but rather stay in the classic setting of temporal models.3.2SemanticsIn what follows,we present the semantics for the notion of entailment for tem-poral graphs based on the corresponding notion for RDF graphs.Definition 2(Temporal Entailment).Let G 1,G 2be RDF temporal graphs.Define–For ground temporal RDF graphs G 1,G 2define G 1|=t G 2as G 1(t )|=G 2(t )for each t ;–For general graphs,G 1|=t G 2iffthere exist ground instances µ1(G 1)and µ2(G 2)such that (µ1(G 1))(t )|=(µ2(G 2))(t )for each t .Note that the definition for ground graphs resembles classical temporal defi-nitions:Proposition 1.Let G 1,G 2be temporal graphs.Then,G 1|=t G 2implies G 1(t )|=G 2(t )for all t ,and the converse is true for ground graphs.In fact,the problems for general graphs are introduced by blank nodes and the notion of entailment.For example,G 1(t )|=G 2(t )for all t does not imply G 1|=t G 2(see Figure 4).We have the following issues:–A blank node represents the same (unnamed)resource throughout the time range,rather than a sequence of different resources.This makes the behavior of temporal marks in Temporal RDF different from the classical setting.Temporal marks here –contrary to temporal XML for example–are not only a relation among fixed objects ,but also among time-varying objects ,the blank nodes.See example in Figure 4.–The notion of entailment for temporal RDF needs a basic arithmetic of inter-vals in order to combine the notion of temporality and deductive properties.For example if we have (a,sc ,c ):[2,3],(c,sc ,d ):[2],then we should be able to derive (a,sc ,d ):[2],but not (a,sc ,d ):[3].In the rest of this section,we show that the notions of closure,lean graph,core –fundamental to define notions of normalization of this data–can be extended without difficulty to the temporal setting.(Compare discussion in [10]).The closure of a temporal graph G ,denoted tcl(G ),is a maximal set of temporal triples G over universe(G )plus the RDF vocabulary such that G contains G and is equivalent to it.Proposition 2(Entailment for Temporal graphs).Let G,G 1,G 2be temporal RDF graphs.Then 1.tcl(G )= t (cl(G (t )))t ;2.G 1|=t G 2if and only if tcl(G 1)|=t G 2.A temporal graph G is lean if and only if there is no proper temporal subgraph Gof G such that G |=t G .The core of G ,core(G )is a lean subgraph of G equivalent to it.With these notions,for a temporal RDF graph G we can define –as in the case of RDF graphs–a notion of normal form ,denoted by nf t (G ),as follows:nf t (G )=core t (G )for a temporal closure G of G .The computational complexities of computing the core and testing whether a graph is lean,are asymptotically the same as the case of standard RDF graphs [10].Proposition 3.Let G,G be graphs.1.The problem of deciding if G is the closure of G is DP-complete.2.The problem of deciding if G is the normal form of G is DP-complete.4Syntax and Deductive System for Temporal GraphsWe present a deductive system for temporal RDF.It is based on a sound and complete set of rules given in [12],plus three rules capturing temporal issues.4.1RDF syntax of temporal triplesDefinition 3(Temporal vocabulary).The temporal vocabulary is the follow-ing:temporal (abbreviated as tpl ),instant ,interval ,initial and final ,all of type property ,and now of type plain literal.The range of instant ,initial and final is the set of natural numbers.We will use the following notation shortcuts:reif(a,b,c,X):the set of triples (X,tsubj,a),(X,tpred,b),(X,tobj,c)(a kind of“temporal reification”of(a,b,c)).5 Definition4(Temporal triples and graphs).Temporal triples are the fol-lowing graphs using the temporal vocabulary.–(a,b,c),reif(a,b,c,X),(X,tpl,Y),(Y,instant,n)where n is a natural num-ber;we will summarize this as(a,b,c):[X,Y,n];–(a,b,c),reif(a,b,c,X),(X,tpl,Y),(Y,interval,Z),(Z,initial,I), (Z,final,F);where I,F are natural number;we will summarize this as (a,b,c):[X,Y,I,F];A temporal graph will be defined as a merge of a set of temporal triples.Because RDF is extensible,nothing prevents the use of the blank nodes included in the definition as target or source of other properties beyond the temporal vocabulary.We want to have a definition of temporal triple independent of the blank nodes occurring in the proposed syntactic definition of temporal triples,e.g.,we want that(a,b,c):[X,Y,n]be essentially equivalent to(a,b,c): [n].Both previous issues are overcame in our syntax by adding certain rules, which regulate the temporal vocabulary.4.2RulesThe set of rules is arranged in four groups.Groups A,B,C,and D are intended to describe the classical RDFS semantics,and we follow the approach in[10]. We omit another group of rules that has to do with internal relationships of the RDF model itself and that we do not consider in this paper.The novelty here is Group T(temporal rules),whose main objective is to be able to standardize the interval version and the instant version as well as help defining“absolute”temporal marks.GROUP A(Existential)For a mapµ:G →G,GGGROUP B(Subproperty)(a,type,property),(a,sp,b)(b,sp,c),(a,sp,b)(x,a,y)GROUP C(Subclass)(a,type,class),(a,sc,b)(b,sc,c),(a,sc,b)(x,type,a)GROUP D(Typing)(a,dom,c)(x,a,y) (x,type,c)(a,range,d)(x,a,y) (y,type,d)5We could have used here the standard reification vocabulary of RDF.We chose not to in order to stress the fact that the notions presented in this paper are independent of any view one may have about the concept of reification in RDF.GROUP T(Temporal)(i2t){(X,tpl,Y),(Y,instant,n):n∈[t1,t2]} (X,tpl,Y),(Y,int,Z),(Z,initial,t1),(Z,final,t2)(t2i)(X,tpl,Y),(Y,int,Z),(Z,initial,t1),(Z,final,t2),n∈[t1,t2] (abs)(a,b,c):[X1,Y1,n1],(a,b,c):[X2,Y2,n2](a,b,c):[U,V,n1],(a,b,c):[U,V,n2],U,V freshRules(i2t)(interval to instants)and(t2i)are needed to standardize the interval version and the instant version,by making them equivalent.Rule(abs) essentially says that marks(instants)can be collected in a single node.This permits to concentrate on temporal marks independent of other contexts in which the variables involving temporal vocabulary are immersed.The definition behaves well in the sense of the following lemma.Lemma2. 1.There exist blanks X,Y such that G|=t(a,b,c):[X,Y,t1,t2] if and only if there exist blanks U,V such that∀j with t1≤j≤t2G|=t (a,b,c):[U,V,t j]2.There exist blanks X1,Y1,X2,Y2such that G|=t(a,b,c):[X1,Y1,t1]andG|=t(a,b,c):[X2,Y2,t2]if and only if there exist blanks U,V such that G|=t(a,b,c):[U,V,t1]and G|=t(a,b,c):[U,V,t2].For a temporal RDF graph G,define G∗as the RDF graph{(a,b,c): [X t,Y t,t]|(a,b,c):[t]∈G},where X t,Y t are free blank variables,different for each t.Conversely,for each RDF graph G with temporal vocabulary,define G∗as the temporal graph defined as{(a,b,c):[t]|∃X∃Y(a,b,c):[X,Y,t]∈G}. Theorem1. 1.Let G1,G2be temporal RDF graphs.Then G1|=t G2implies G∗1|=G∗2.2.Let G1,G2be RDF graphs with temporal vocabulary.Then G1|=G2implies(G1)∗|=t(G2)∗.3.Let G be a temporal RDF graph,and G an RDF graph with temporal vocab-ulary.Then(G∗)∗=G and G |=(G ∗)∗.Now we can show that the syntax introduced captures the semantics of tem-poral RDF.The following deductive system based on the rules presented,is sound and complete for entailment of RDF graphs with rdfs vocabulary.Definition5.Let G be a graph.For each rule r:AB above,define G r G∪µ(B)iffthere is a mapµ:A→G.Also define G s G if and only if G is a subgraph of G.Define G G if there is afinite sequence of graphs G1,...,G n such that(1) G=G1;(2)G =G n;and(3)for each i,either,G i r G i+1for some r,or G i s G i+1.The following theorem shows that one can give a syntactic characterization over RDF graphs with temporal vocabulary for entailment of temporal RDF graphs:Theorem2.For any pair of temporal RDF graphs G1,G2:G1|=t G2if and only if G∗1 G∗2.Note that that we cannot establish the theorem in its complete generality, namely,to prove that for RDF graphs G1,G2with temporal vocabulary,G1 G2 if and only if(G1)∗|=t(G2)∗.(Both graphs in Figure4have identical()∗-images but are not -equivalent.)The previous theorem permits to concentrate for the following sections in temporal RDF(instead of diving into syntactic issues).5Query languageIn this section we present query language for temporal RDF graphs,along with its semantics.We also present a brief study of the complexity of query processing.5.1The Query Language by ExampleWe will give theflavor of the query language using our running example,the database of Figure2.Let us begin with a simple query:“Find students who have taken a Master course between year2000and now and return them qualified by 21-century-student”.This query can be expressed as:(?X,type,21-century-student)←(?X,takes,?C):[?T],(?C,type,Master):[?T],2000≤?T,?T≤Now.This example query illustrates the need of a built-in arithmetic language in order to reason about time and intervals.Another important observation is that temporal queries may output non-temporal RDF graph,as the previous query does.For the query asking for a snapshot of the graph at t1,we have:(?X,?Y,?Z)←(?X,?Y,?Y):[t1].Now consider the query“Students taking Ph.D courses together,and the time instants when this occurred.”For simplicity we expressed this as a point-based query.The translation of the result into intervals is straightforward.(?X,together,?Y)[?T]←(?X,type,P h.D):[?T],(?Y,type,P h.D):[?T].Next,we give examples of queries that use temporal triples with intervals. The query“Time intervals when the IT Master was offered”can be expressed as follows:(X,interval,Y),(Y,initial,T i),(Y,final,T f)←(IT Master,sc,Prof.Master):[T i,T f].Observe that the previous query returns a set of intervals.In order to retrieve maximal intervals we need a more subtle query,since their computation do not follow from the temporal rules.For the query“Compute the maximal interval when the triple(a,b,c)holds”,we need aggregate operators MAX and MIN. (a,b,c):[?T1,?T2]←(a,b,c):[?T i,?T f],?T1=MIN(?T i),?T2=MAX(?T f)For a query asking for“Students applying for jobs at time t afterfinishing their Ph.D.program in no more than4years”,we have:(?X,apply,job)←(X,type,Ph.D): t i,t f ,t f−t i<4,t f<t.Here,the notation t i,t f stands that t i and t f match with the maximal interval for the corresponding triple computed with the query given above.5.2Semantics and ComplexityLet V be a set of variables(disjoint from UBLT).Individual variables will be denoted?X,?Y,?Z,etc.There is also a set of temporal variables V t⊂V.The query language we define is analogous to the one presented by Gutierrez et al.[11].A query is a temporal tableau,which is a pair(H,B∪A),where H and B are temporal RDF graphs with some elements of UBL replaced by variables in V,and with some elements of T replaced with variables in V t,B has no blank nodes and all the variables in H occur also in B.The set A has the usual arithmetic built-in predicates such as<,>,=,.over elements in V t and T.We adopt the usual notion of safe rule from Datalog to prevent operations on infinite predicates.A rule is safe if all its variables are limited.A variable is limited if one of the following hold:a variable appears as an argument in a non-built-in predicate of the body;the variable X appears in a subgoal X=t (or t=X),where t is a constant in T;or the variable X appears in a subgoal X=Y(or Y=X),where Y is limited.The semantics is the usual in these cases.Given a temporal tableau(H,B∪A) and a temporal RDF graph G,for each matching of the graph pattern B in G, pick up the values of the variables and check whether they satisfy the built-in predicates in A.If this is the case,construct a pre-answer,which is the graph resulting by substituting the values of the variables in the head.Finally,the answer of the query is the union of all pre-answers.We end this section by showing that the additional time dimension in our model does not play any relevant role in the complexity of query answering,that is,the query language preserves the tractability of answers.In order to do this, we consider the simpler problem of testing emptiness of the query answer set in the following forms:(1)Query complexity version:For afixed database D,given a query q,is q(D)non-empty?(2)Data complexity version:For afixed query q, given a database D,is q(D)non-empty?Theorem3.The evaluation problem is NP-complete for the query complexity version,and polynomial for the data complexity version.。

ELSEVIER PII: SOOlO-4485(97)00101-2 Computer-Aided Design, Vol. 30, No. 5, pp. 377-389, 1998 8 1998 Elsevier Science Ltd. All rights reserved Printed in Great Britain 0010~4485/98/$19.00+0.cm

Current research in the

conceptual design of mechanical products

Wynne Hsu* and Irene M Y Woon Decisions made at the conceptual design stage have significant influence on factors such as costs, performance, reliability, safety and environmental impact of a product. However, knowledge of all the design requirements and constraints during this early phase of a product’s life cycle is usually imprecise, approximate or unknown. Faced with such complexity, individual designers have restricted themselves to narrow, well-defined sub-tasks and as a result, progress in this area has been patchy and spasmodic. The purpose of this survey is to document the current state of research and development in this crucial design activity and in doing so, to

Inference is a good guess heuristics (based on logic, statistics etc.) to observations or by interpolating the next logical step in an intuited pattern. The conclusion drawn is also called an inference. The laws of valid inference are studied in the field of logic.Human inference (i.e. how humans draw conclusions) is traditionally studied within the field of cognitive psychology; artificial intelligence researchers develop automated inference systems to emulate human inference. Statistical inference allows for inference from quantitative data.Contents[hide]∙ 1 Accuracy of inductive inferences∙ 2 Examples of deductive inference∙ 3 Incorrect inference∙ 4 Automatic logical inferenceo 4.1 Example using Prologo 4.2 Use with the semantic webo 4.3 Bayesian statistics and probability logico 4.4 Nonmonotonic logic[1]∙ 5 See also∙ 6 References[edit] Accuracy of inductive inferencesThe process by which a conclusion is inferred from multiple observations is called inductive reasoning. The conclusion may be correct or incorrect, or correct to within a certain degree of accuracy, or correct in certain situations. Conclusions inferred from multiple observations may be tested by additional observations.[edit] Examples of deductive inferenceGreek philosophers defined a number of syllogisms, correct three part inferences, that can be used as building blocks for more complex reasoning. We begin with the most famous of them all:1.All men are mortal2.Socrates is a man3.Therefore, Socrates is mortal.The reader can check that the premises and conclusion are true, but Logic is concerned with inference: does the truth of the conclusion follow from that of the premises?The validity of an inference depends on the form of the inference. That is, the word "valid" does not refer to the truth of the premises or the conclusion, but rather to the form of the inference. An inference can be valid even if the parts are false, and can be invalid even if the parts are true. But a valid form with true premises will always have a true conclusion.For example, consider the form of the following symbological track:1.All apples are blue.2. A banana is an apple.3.Therefore, a banana is blue.For the conclusion to be necessarily true, the premises need to be true. Now we turn to an invalid form.1.All A are B.2. C is a B.3.Therefore, C is an A.To show that this form is invalid, we demonstrate how it can lead from true premises to a false conclusion.1.All apples are fruit. (True)2.Bananas are fruit. (True)3.Therefore, bananas are apples. (False)A valid argument with false premises may lead to a false conclusion:1.All fat people are Greek.2.John Lennon was fat.3.Therefore, John Lennon was Greek.When a valid argument is used to derive a false conclusion from false premises, the inference is valid because it follows the form of a correct inference.A valid argument can also be used to derive a true conclusion from false premises:1.All fat people are musicians2.John Lennon was fat3.Therefore, John Lennon was a musicianIn this case we have two false premises that imply a true conclusion. [edit] Incorrect inferenceAn incorrect inference is known as a fallacy. Philosophers who study informal logic have compiled large lists of them, and cognitive psychologists have documented many biases in human reasoning that favor incorrect reasoning.[edit] Automatic logical inferenceAI systems first provided automated logical inference and these were once extremely popular research topics, leading to industrial applications under the form of expert systems and later business rule engines.An inference system's job is to extend a knowledge base automatically. The knowledge base (KB) is a set of propositions that represent what the system knows about the world. Several techniques can be used by that system to extend KB by means of valid inferences. An additional requirement is that the conclusions the system arrives at are relevant to its task.[edit] Example using PrologProlog (for "Programming in Logic") is a programming language based on a subset of predicate calculus. Its main job is to check whether a certain proposition can be inferred from a KB (knowledge base) using an algorithm called backward chaining.Let us return to our Socrates syllogism. We enter into our Knowledge Base the following piece of code:mortal(X) :- man(X).man(socrates).( Here :-can be read as if. Generally, if P Q(if P then Q) then in Prolog we would code Q:-P (Q if P).)This states that all men are mortal and that Socrates is a man. Now we can ask the Prolog system about Socrates:?- mortal(socrates).(where ?- signifies a query: Can mortal(socrates). be deduced from the KB using the rules) gives the answer "Yes".On the other hand, asking the Prolog system the following:?- mortal(plato).gives the answer "No".This is because Prolog does not know anything about Plato, and hence defaults to any property about Plato being false (the so-called closed world assumption). Finally ?- mortal(X) (Is anything mortal) would result in "Yes" (and in some implementations: "Yes": X=socrates)Prolog can be used for vastly more complicated inference tasks. See the corresponding article for further examples.[edit] Use with the semantic webRecently automatic reasoners found in semantic web a new field of application. Being based upon first-order logic, knowledge expressed using one variant of OWL can be logically processed, i.e., inferences can be made upon it.[edit] Bayesian statistics and probability logicPhilosophers and scientists who follow the Bayesian framework for inference use the mathematical rules of probability to find this best explanation. The Bayesian view has a number of desirable features—one of them is that it embeds deductive (certain) logic as a subset (this prompts some writers to call Bayesian probability "probability logic", following E. T. Jaynes).Bayesians identify probabilities with degrees of beliefs, with certainly true propositions having probability 1, and certainly false propositions having probability 0. To say that "it's going to rain tomorrow" has a 0.9probability is to say that you consider the possibility of rain tomorrow as extremely likely.Through the rules of probability, the probability of a conclusion and of alternatives can be calculated. The best explanation is most often identified with the most probable (see Bayesian decision theory). A central rule of Bayesian inference is Bayes' theorem, which gave its name to the field.See Bayesian inference for examples.[edit] Nonmonotonic logic[1]A relation of inference is monotonic if the addition of premises does not undermine previously reached conclusions; otherwise the relation is nonmonotonic. Deductive inference, is monotonic: if a conclusion is reached on the basis of a certain set of premises, then that conclusion still holds if more premises are added.By contrast, everyday reasoning is mostly nonmonotonic because it involves risk: we jump to conclusions from deductively insufficient premises. We know when it is worth or even necessary (e.g. in medical diagnosis) to take the risk. Yet we are also aware that such inference is defeasible—that new information may undermine old conclusions. Various kinds of defeasible but remarkably successful inference have traditionally captured the attention of philosophers (theories of induction, Peirce’s theory of abduction, inference to the best explanation, etc.). More recently logicians have begun to approach the phenomenon from a formal point of view. The result is a large body of theories at the interface of philosophy, logic and artificial intelligence.[edit] See also∙Reasoningo Abductive reasoningo Deductive reasoningo Inductive reasoningo Retroductive reasoning ∙Analogy∙Axiom∙Bayesian inference∙Business rule ∙Fuzzy logic∙Immediateinference∙Inference engine∙Inquiry∙Logic∙Logic ofinformation∙Logical assertion∙Business rules engine ∙Expert system ∙Logical graph∙Nonmonotonic logic ∙Rule of inference ∙List of rules of inference∙Theorem∙Sherlock Holmes[edit] References1.^Fuhrmann, André. Nonmonotonic Logic.http://www.uni-konstanz.de/FuF/Philo/Philosophie/Fuhrmann/papers/nomoLog.pdf.∙Hacking, Ian (2000). An Introduction to Probability and Inductive Logic. Cambridge University Press. ISBN0521775019.∙Jaynes, Edwin Thompson (2003). Probability Theory: The Logic of Science. Cambridge University Press. ISBN0-521-59271-2./catalogue.asp?isbn=0521592712.∙McKay, David J.C. (2003). Information Theory, Inference, and Learning Algorithms. Cambridge University Press.ISBN0-521-64298-1./mackay/itila/book.html.∙Russell, Stuart J.; Norvig, Peter(2003), Artificial Intelligence:A Modern Approach (2nd ed.), Upper Saddle River, New Jersey:Prentice Hall, ISBN0-13-790395-2, /∙Tijms, Henk (2004). Understanding Probability. Cambridge University Press. ISBN0521701724.Retrieved from "/wiki/Inference"Categories: Logic and statistics | Sources of knowledge | Reasoning | Concepts in logic | Logical consequenceHidden categories: Logic articles needing expert attention | Articles needing expert attention from November 2008| All articles needing expert attention | Articles lacking in-text citations from April 2010 | All articles lacking in-text citationsPersonal tools∙Log in / create accountNamespaces∙Article∙DiscussionVariantsViews∙Read∙Edit∙View historyActionsSearchNavigation∙Main page∙Contents∙Featured content∙Current events∙Random article∙Donate to Wikipedia Interaction∙Help∙About Wikipedia∙Community portal∙Recent changes∙Contact Wikipedia Toolbox∙What links here∙Related changes∙Upload file∙Special pages∙Permanent link∙Cite this pagePrint/export∙Create a book∙Download as PDF∙Printable version Languages∙ةيبرعلا∙Български∙Català∙Deutsch∙Español∙Esperanto∙Français∙한국어∙Hrvatski∙Italiano∙Nederlands∙日本語∙Polski∙Português∙Română∙Русский∙This page was last modified on 4 December 2010 at 00:02.∙Text is available under the Creative CommonsAttribution-ShareAlike License; additional terms may apply. See Terms of Use for details.Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc., a non-profit organization.∙Contact us∙Privacy policy∙About Wikipedia∙Disclaimers∙∙。

Inference is the act of drawing a conclusion by deductive reasoning from given facts. The conclusion drawn is also called an inference. The laws of valid inference are studied in the field of logic.Human inference (i.e. how humans draw conclusions) is traditionally studied within the field of cognitive psychology; artificial intelligence researchers develop automated inference systems to emulate human inference. Statistical inference allows for inference from quantitative data.Contents[hide]∙ 1 Accuracy of inductive inferences∙ 2 Examples of deductive inference∙ 3 Incorrect inference∙ 4 Automatic logical inferenceo 4.1 Example using Prologo 4.2 Use with the semantic webo 4.3 Bayesian statistics and probability logico 4.4 Nonmonotonic logic[1]∙ 5 See also∙ 6 References[edit] Accuracy of inductive inferencesThe process by which a conclusion is inferred from multiple observations is called inductive reasoning. The conclusion may be correct or incorrect, or correct to within a certain degree of accuracy, or correct in certain situations. Conclusions inferred from multiple observations may be tested by additional observations.[edit] Examples of deductive inferenceGreek philosophers defined a number of syllogisms, correct three part inferences, that can be used as building blocks for more complex reasoning. We begin with the most famous of them all:1.All men are mortal2.Socrates is a man3.Therefore, Socrates is mortal.The reader can check that the premises and conclusion are true, but Logic is concerned with inference: does the truth of the conclusion follow from that of the premises?The validity of an inference depends on the form of the inference. That is, the word "valid" does not refer to the truth of the premises or the conclusion, but rather to the form of the inference. An inference can be valid even if the parts are false, and can be invalid even if the parts are true. But a valid form with true premises will always have a true conclusion.For example, consider the form of the following symbological track:1.All apples are blue.2. A banana is an apple.3.Therefore, a banana is blue.For the conclusion to be necessarily true, the premises need to be true.Now we turn to an invalid form.1.All A are B.2. C is a B.3.Therefore, C is an A.To show that this form is invalid, we demonstrate how it can lead from true premises to a false conclusion.1.All apples are fruit. (True)2.Bananas are fruit. (True)3.Therefore, bananas are apples. (False)A valid argument with false premises may lead to a false conclusion:1.All fat people are Greek.2.John Lennon was fat.3.Therefore, John Lennon was Greek.When a valid argument is used to derive a false conclusion from false premises, the inference is valid because it follows the form of a correct inference.A valid argument can also be used to derive a true conclusion from false premises:1.All fat people are musicians2.John Lennon was fat3.Therefore, John Lennon was a musicianIn this case we have two false premises that imply a true conclusion.[edit] Incorrect inferenceAn incorrect inference is known as a fallacy. Philosophers who study informal logic have compiled large lists of them, and cognitive psychologists have documented many biases in human reasoning that favor incorrect reasoning.[edit] Automatic logical inferenceAI systems first provided automated logical inference and these were once extremely popular research topics, leading to industrial applications under the form of expert systems and later business rule engines.An inference system's job is to extend a knowledge base automatically. The knowledge base (KB) is a set of propositions that represent what the system knows about the world. Several techniques can be used by that system to extend KB by means of valid inferences. An additional requirement is that the conclusions the system arrives at are relevant to its task.[edit] Example using PrologProlog (for "Programming in Logic") is a programming language based on a subset of predicate calculus. Its main job is to check whether a certain proposition can be inferred from a KB (knowledge base) using an algorithm called backward chaining.Let us return to our Socrates syllogism. We enter into our Knowledge Base the following piece of code:mortal(X) :- man(X).man(socrates).( Here :-can be read as if. Generally, if P Q(if P then Q) then in Prolog we would code Q:-P (Q if P).)This states that all men are mortal and that Socrates is a man. Now we can ask the Prolog system about Socrates:?- mortal(socrates).(where ?- signifies a query: Can mortal(socrates). be deduced from the KB using the rules) gives the answer "Yes".On the other hand, asking the Prolog system the following:?- mortal(plato).gives the answer "No".This is because Prolog does not know anything about Plato, and hence defaults to any property about Plato being false (the so-called closed world assumption). Finally ?- mortal(X) (Is anything mortal) would result in "Yes" (and in some implementations: "Yes": X=socrates)Prolog can be used for vastly more complicated inference tasks. See the corresponding article for further examples.[edit] Use with the semantic webRecently automatic reasoners found in semantic web a new field of application. Being based upon first-order logic, knowledge expressed using one variant of OWL can be logically processed, i.e., inferences can be made upon it.[edit] Bayesian statistics and probability logicPhilosophers and scientists who follow the Bayesian framework for inference use the mathematical rules of probability to find this best explanation. The Bayesian view has a number of desirable features—one of them is that it embeds deductive (certain) logic as a subset (this prompts some writers to call Bayesian probability "probability logic", following E. T. Jaynes).Bayesians identify probabilities with degrees of beliefs, with certainly true propositions having probability 1, and certainly false propositions having probability 0. To say that "it's going to rain tomorrow" has a 0.9 probability is to say that you consider the possibility of rain tomorrow as extremely likely.Through the rules of probability, the probability of a conclusion and of alternatives can be calculated. The best explanation is most often identified with the most probable (see Bayesian decision theory). Acentral rule of Bayesian inference is Bayes' theorem, which gave its name to the field.See Bayesian inference for examples.[edit] Nonmonotonic logic[1]A relation of inference is monotonic if the addition of premises does not undermine previously reached conclusions; otherwise the relation is nonmonotonic. Deductive inference, is monotonic: if a conclusion is reached on the basis of a certain set of premises, then that conclusion still holds if more premises are added.By contrast, everyday reasoning is mostly nonmonotonic because it involves risk: we jump to conclusions from deductively insufficient premises. We know when it is worth or even necessary (e.g. in medical diagnosis) to take the risk. Yet we are also aware that such inference is defeasible—that new information may undermine old conclusions. Various kinds of defeasible but remarkably successful inference have traditionally captured the attention of philosophers (theories of induction, Peirce’s theory of abduction, inference to the best explanation, etc.). More recently logicians have begun to approach the phenomenon from a formal point of view. The result is a large body of theories at the interface of philosophy, logic and artificial intelligence.[edit] See also∙Reasoningo Abductive reasoningo Deductive reasoningo Inductive reasoningo Retroductive reasoning ∙Entailment∙Analogy∙Axiom∙Bayesian inference∙Business rule∙Business rules engine ∙Fuzzy logic∙Immediate inference∙Inference engine∙Inquiry∙Logic∙Logic of information∙Logical assertion∙Logical graph∙Nonmonotonic logic∙Rule of inference∙List of rules of inference ∙Theorem∙Expert system∙Sherlock Holmes。

• we have identified the problems of adapting the technique to C++ and we give solutions to them,
• we give the complete formal algorithm of the technique, and • using a prototype implementation, we show the effect of the algorithm on
Annales Univ. Sci. Budapest., Sect. Comp. 30 (20 C++ PROGRAMS VIA CONTROL FLOW FLATTENING
T. L´aszl´o and A´ . Kiss (Szeged, Hungary)
test programs.
The remaining part of the paper is structured as follows. In Section 2 we give a detailed description of the problems that occured during the adaptation of the technique to C++ and we offer solutions to them. Moreover, we also give the complete formal algorithm of the proposed technique. Next, in Section 3, we present our experimental results. In Section 4 we present an overview of the related works, and finally, in Section 5 we summarize our results and conclude the paper.

《离散数学》双语专业词汇表set：集合subset：子集element, member：成员，元素well-defined：良定，完全确定brace：花括号representation：表示sensible：有意义的rational number：有理数empty set：空集Venn diagram：文氏图contain(in)：包含（于）universal set：全集finite (infinite) set：有限（无限）集cardinality：基数，势power set：幂集operation on sets：集合运算disjoint sets：不相交集intersection：交union：并complement of B with respect to A：A与B的差集symmetric difference：对称差commutative：可交换的associative：可结合的distributive：可分配的idempotent：等幂的de Morgan’s laws：德摩根律inclusion-exclusion principle：容斥原理sequence：序列subscript：下标recursive：递归explicit：显式的string：串，字符串set corresponding to a sequence：对应于序列的集合linear array(list)：线性表characteristic function：特征函数countable(uncountable)：可数（不可数）alphabet：字母表word：词empty sequence(string)：空串catenation：合并，拼接regular expression：正则表达式division：除法multiple：倍数prime：素（数）algorithm：算法common divisor：公因子GCD(greatest common divisor)：最大公因子LCM(least common multiple)：最小公倍数Euclidian algorithm：欧几里得算法，辗转相除法pseudocode：伪码（拟码）matrix：矩阵square matrix：方阵row：行column：列entry(element)：元素diagonal matrix：对角阵Boolean matrix：布尔矩阵join：并meet：交Boolean product：布尔乘积mathematical structure(system)：数学结构（系统）closed with respect to：对…是封闭的binary operation：二元运算unary operation：一元运算identity：么元，单位元inverse：逆元statement, proposition：命题logical connective：命题联结词compound statement：复合命题propositional variable：命题变元negation：否定（式）truth table：真值表conjunction：合取disjunction：析取quantifier：量词universal quantification：全称量词化propositional function：命题公式predicate：谓词existential quantification：存在量词化converse：逆命题conditional statement, implication：条件式，蕴涵式consequent, conclusion：结论，后件contrapositive：逆否命题hypothesis：假设，前提，前件biconditional, equivalence：双条件式，等价logically equivalent：（逻辑）等价的contingency：可满足式tautology：永真(重言)式contradiction, absurdity：永假(矛盾)式logically follow：是…的逻辑结论rules of reference：推理规则modus ponens：肯定律m odus tollens：否定律indirect method：间接证明法proof by contradiction：反证法counterexample；反例basic step：基础步principle of mathematical induction：（第一）数学归纳法induction step：归纳步strong induction：第二数学归纳法relation：关系digraph：有向图ordered pair：有序对，序偶product set, Caretesian set：叉积，笛partition, quotient set：划分，商集block, cell：划分块，单元domain：定义域range：值域R-relative set：R相关集vertex(vertices)：结点，顶点edge：边in-degree：入度out-degree：出度path：通路，路径cycle：回路connectivity relation：连通性关系reachability relation：可达性关系composition：复合reflexive：自反的irreflexive：反自反的empty relation：空关系symmetric：对称的asymmetric：非对称的antisymmetric：反对称的graph：无向图undirected edge：无向边adjacent vertices：邻接结点connected：连通的transitive：传递的equivalent relation：等价关系congruent to：与…同余modulus：模equivalence class：等价类linked list：链表storage cell：存储单元pointer：指针complementary relation：补关系inverse：逆关系closure：闭包symmetric closure：对称闭包reflexive closure：自反闭包composition：关系的复合transitive closure：传递闭包Warshal’s algorithm：Warshall算法function, mapping, transformation：函数，映射，变换argument：自变量value, image：值，像，应变量labeled digraph：标记有向图identity function on A：A上的恒等函数everywhere defined：处处有定义的onto：到上函数，满射one to one：单射，一对一函数bijection, one-to-one correspondence：双射，一一对应invertible function：可逆函数floor function：下取整函数ceiling function：上取整函数Boolean function：布尔函数base 2 exponential function：以2为底的指数函数logarithm function to the base n：以n为底的对数hashing function：杂凑函数key：键growth of function：函数增长same order：同阶lower order：低阶running time：运行时间permutation：置换，排列cyclic permutation：循环置换，轮换transposition：对换odd(even) permutation：奇（偶）置换order relation：序关系partial order：偏序关系partially ordered set, poset：偏序集dual：对偶comparable：可比较的linear order(total order)：线序，全序linearly ordered set, chain：线（全）序集，链product partial order：积偏序lexicographic order：字典序Hasse diagram：哈斯图topological sorting：拓扑排序isomorphism：同构maximal(minimal) element：极大(小)元extremal element：极值元素greatest(least) element：最大(小)元unit element：么(单位)元zero element：零元upper(lower) bound：上(下)界least upper(greatest lower) bound：上(下)确界lattice：格join：，保联，并meet：保交，交sublattice：子格absorption property：吸收律bounded lattice：有界格distributive lattice：分配格complement：补元modular lattice：模格Boolean algebra：布尔代数involution property：对合律Boolean polynomial, Boolean expression：布尔多项式（表达式）or(and, not) gate：或(与，非)门inverter：反向器circuit design：线路设计minterm：极小项Karnaugh map：卡诺图tree：树root：根，根结点rooted tree：（有）根树level：层，parent：父结点offspring：子女结点siblings：兄弟结点height：树高leaf(leave)：叶结点ordered tree：有序树n-tree：n-元树complete n-tree：完全n-元树(complete) binary tree：(完全)二元(叉)树descendant：后代subtree：子树positional tree：位置树positional binary tree：位置二元(叉)树doubly linked list：双向链表tree searching：树的搜索（遍历）traverse：遍历，周游preorder search：前序遍历Polish form：（表达式的）波兰表示inorder search：中序遍历postorder search：后序遍历reverse Polish form：（表达式的）逆波兰表示linked-list representation：链表表示undirected tree：无向树undirected edge：无向边adjacent vertices：邻接结点simple path：简单路径（通路）simple cycle：简单回路acyclic：无（简单）回路的spanning tree：生成树，支撑树Prim’s algorithm：Prim算法minimal spanning tree：最小生成树weighted graph：（赋）权图weight：树distance：距离nearest neighbor：最邻近结点greedy algorithm：贪婪算法optimal solution：最佳方法Kruskal’s algorithm：Kruskal算法graph：(无向)图vertex(vertices)：结点edge：边end point：端点relationship：关系connection：连接degree of a vertex：结点的度loop：自回路path：路径isolated vertex：孤立结点adjacent vertices：邻接结点circuit：回路simple path(circuit)：基本路径(回路) connected：连通的disconnected：不连通的component：分图discrete graph(null graph)：零图complete graph：完全图regular graph：正规图，正则图linear graph：线性图subgraph：子图Euler path(circuit)：欧拉路径(回路) Konisberg Bridge problem：哥尼斯堡七桥问题ordinance：法规recycle：回收，再循环bridge：桥，割边Hamiltonian path(circuit)：哈密尔顿路径(回路)dodecahedron：正十二面体weight：权TSP(traveling salesperson problem)：货郎担问题transport network：运输网络capacity：容量maximum flow：最大流source：源sink：汇conversation of flow：流的守恒value of a flow：流的值excess capacity：增值容量cut：割the capacity of a cut：割的容量matching problems：匹配问题matching function：匹配函数compatible with：与…相容maximal match：最大匹配complete match：完全匹配coloring graphs：图的着色proper coloring：正规着色chromatic number of G：G的色数map-coloring problem：地图着色问题conjecture：猜想planar graph：(可)平面图bland meats：未加调料的肉chromatic polynomial：着色多项式binary operation on a set A：集合A上的二元运算closed under the operation：运算对…是封闭的commutative：可交换的associative：可结合的idempotent：幂等的distributive：可分配的semigroup：半群product：积free semigroup generated by A：由A生成的自由半群identity(element)：么（单位）元monoid：含么半群，独异点subsemigroup：子半群submonoid：子含么半群isomorphism：同构homomorphism：同态homomorphic image：同态像Kernel：同态核congruence relation：同余关系natural homomorphism：自然同态group：群inverse：逆元quotient group：商群Abelian group：交换（阿贝尔）群cancellation property：消去律multiplication table：运算表finite group：有限（阶）群order of a group：群的阶symmetric group：对称群subgroup：子群alternating group：交替群Klein 4 group：Klein四元群coset：陪集(left) right coset：(左)右陪集normal subgroup：正规(不变)子群prerequisite：预备知识virtually：几乎informal brand：不严格的那种notation：标记sensible：有意义的logician：逻辑学家extensively：广泛地，全面地commuter：经常往来于两地的人by convention：按常规，按惯例dimension：维(数) compatible：相容的discipline：学科reasoning：推理declarative sentence：陈述句n-tuple：n-元组component sentence：分句tacitly：默认generic element：任一元素algorithm verification：算法证明counting：计数factorial：阶乘combination：组合pigeonhole principle：鸽巢原理existence proof：存在性证明constructive proof：构造性证明category：类别，分类factor：因子consecutively：相继地probability(theory)：概率(论) die：骰子probabilistic：概率性的sample space：样本空间event：事件certain event：必然事件impossible event：不可能事件mutually exclusive：互斥的，不相交的likelihood：可能性frequency of occurrence：出现次数(频率) summarize：总结，概括plausible：似乎可能的equally likely：等可能的，等概率的random selection(choose an object at random)：随机选择terminology：术语expected value：期望值backtracking：回溯characteristic equation：特征方程linear homogeneous relation of degree k：k阶线性齐次关系binary relation：二元关系prescribe：命令，规定coordinate：坐标criteria：标准，准则gender：性别graduate school：研究生院generalize：推广notion：概念intuitively：直觉地verbally：用言语approach：方法，方式conversely：相反地pictorially：以图形方式restriction：限制direct flight：直飞航班tedious：冗长乏味的main diagonal：主对角线remainder：余数random access：随机访问sequential access：顺序访问custom：惯例polynomial：多项式substitution：替换multi-valued function：多值函数collision：冲突analysis of algorithm：算法分析sophisticated：复杂的set inclusion(containment)：集合包含distinguish：区分analogous：类似的ordered triple：有序三元组recreational area：游乐场所multigraph：多重图pumping station：抽水站depot：货站，仓库relay station：转送站。

《×××××》教学大纲（如是双语或全英课程应提供中文和英文教学大纲）总学时：理论课学时：实验课学时：学分：一、课程的性质二、课程的目的与教学基本要求三、课程适用专业四、课程的教学内容、要求与学时分配（一）1.（1）a.1．理论教学部分按各章节列出主要内容，注明课程教学的难点和重点，对学生掌握知识的要求，以及学时的分配。

2．实验教学部分列出实验名称（实验项目）、学时分配，明确具体内容，对学生的要求等。

五、教材和主要参考资料六、课程考核方式备注：（如果有要求先修课程请在此处列出）《×××××》Course DescriptionTotal Hours：Lecture Hours：Experimental Hours：1.Characteristic of the Course“必修课”翻译为：Compulsory Course“选修课”翻译为：Elective Course2.Aim of the Course and the Basic Requirements3.Applicable Speciality4.Course content, Requirements and Hours Allocation（1）a.(1) Lecture按各章节列出主要内容，注明课程教学的难点和重点，对学生掌握知识的要求，以及学时的分配。

(2) Experiment列出实验名称（实验项目）、学时分配，明确具体内容，对学生的要求等。

5.Textbooks and Main Reference6.Evaluation MethodNotes：（如果有要求先修课程请在此处列出）示例：《线性代数》教学大纲总学时：32 学分：2一、课程的性质公共基础必修课程。

二、课程的目的与教学基本要求线性代数是高等学校本科生重要的公共基础课之一，通过这门课的学习，使学生获得比较全面的线性代数的基本知识和必要的基本运算技能；同时培养学生在运用数学理论分析问题和解决问题的能力，增加数学软件的学习，为学习有关专业基础知识和专业课程及扩大数学知识方面提供必要的数学基础。

英语专业研究生试卷班级__________ 学生名字__________ 分数______《英语专业研究生英语语言文学基础试卷》一、单项选择题（每题2分，共30分）1. Which of the following is NOT a feature of Old English?A. Rich inflectional systemB. Use of the runic alphabetC. Mostly monosyllabic wordsD. Influence from Latin2. The term “metaphor” refers to ________.A. a figure of speech that makes a comparison between two unlike things without using “like” or “as”B. a repetition of initial consonant sounds in neighboring wordsC. a word or phrase that has lost its original meaningD. a story or narrative used to illustrate a moral or religious lesson3. In the sentence “I saw the man with a telescope.”, the prepositional phrase “with a telescope” is ________.A. an adverbial modifierB. an attributive modifierC. a complementD. a part of the predicate4. Which of the following playwrights is associated with the Elizabethan theater?A. Christopher MarloweB. Samuel BeckettC. Henrik IbsenD. Anton Chekhov5. The study of the origin and history of words is called ________.A. semanticsB. morphologyC. etymologyD. syntax6. “To be or not to be, that is the question.” is from which of Shakespeare’s plays?A. HamletB. Romeo and JulietC. MacbethD. Othello7. In English phonetics, the sound /θ/ is produced by ________.A. placing the tip of the tongue between the teethB. vibrating the vocal cords while the tongue is in a certain positionC. raising the back of the tongue towards the soft palateD. rounding the lips and forcing air through a narrow opening8. Which of the following is an example of a compound word?A. beautifulB. blackboardC. runningD. teacher9. The concept of “linguistic relativity” was proposed by ________.A. Noam ChomskyB. Ferdinand de SaussureC. Benjamin Lee WhorfD. Edward Sapir10. A sonnet is a poem that usually consists of ________ lines.A. 12B. 14C. 16D. 1811. Which of the following is a modal verb?A. runB. canC. happyD. book12. In the English language, the stress pattern in the word “photograph” is ________.A. 'photographB. pho'tographC. photo'graphD. pho to'graph13. Which of the following languages has the most influence on the development of Modern English?A. FrenchB. GermanC. GreekD. Latin14. The sentence “She made the boy clean his room.” is an example of ________.A. a simple sentenceB. a compound sentenceC. a complex sentenceD. a catenative construction15. Which of the following literary movements emphasized individualism and the beauty of nature?A. RomanticismB. RealismC. ModernismD. Post - modernism二、阅读理解（每题3分，共30分）Read the following passage and answer the questions:The history of the English language really started with the arrival of three Germanic tribes who invaded Britain during the 5th century AD. These tribes, the Angles, the Saxons and the Jutes, crossed the North Sea from what today is Denmark and northern Germany. At that time the inhabitants of Britain spoke a Celtic language. But most of the Celtic speakers were pushed west and north by the invaders - mainly into what is now Wales, Scotland and Ireland.The Angles came from "Englaland" and their language was called "Englisc" - from which the words "England" and "English" are derived. The invading Germanic tribes spoke similar languages, which in Britain developed into what we now call Old English. Old English did not sound or look like English today. Native English speakers now would have great difficulty understanding Old English. Nevertheless, about half of the most commonly used words in Modern English have Old English roots.Old English was a highly inflected language. This means that words changed their endings depending on their function in the sentence. For example, the word for "stone" was "stan" in the nominative case (when it was the subject of the sentence), but "stane" in the dative case (when it was the indirect object).Over time, the English language has changed a great deal. One of the major influences on English was the Norman Conquest in 1066. The Normans were from France and they brought with them the French language. For a long time, French was the language of the ruling class in England, while English was spoken by the common people. This led to the addition of a large number of French words to the English vocabulary.1. Who invaded Britain in the 5th century AD?2. What happened to the Celtic speakers when the Germanic tribes invaded?3. Where did the Angles come from?4. Why is Old English difficult for modern native English speakers to understand?5. What is meant by "Old English was a highly inflected language"?6. What was the major influence on English after the Norman Conquest in 1066?7. Who spoke French and who spoke English after the Norman Conquest?8. What is the origin of the words "England" and "English"?9. How has the English language changed over time?10. Give an example of how words changed in Old English depending on their function in the sentence.三、简答题（每题10分，共30分）1. Briefly explain the difference between a simile and a metaphor.2. Describe the main features of the Romantic literary movement.3. Explain how language acquisition in children occurs according to one of the major theories.四、Essay Question (10分)Discuss the importance of English as a global language.答案与解析：一、单项选择题1. C. Old English had a rich inflectional system, used the runic alphabet initially and was influenced by Latin. It had many polysyllabic words as well as monosyllabic ones.2. A. A metaphor is a figure of speech making a comparison without using “like” or “as”. B is allite ration, C is semantic change, D is parable.3. A. “with a telescope” in this sentence modifies the verb “saw” and tells how the seeing was done, so it is an adverbial modifier.4. A. Christopher Marlowe was an Elizabethan playwright. Beckett is a modernist, Ibsen is Norwegian and Chekhov is Russian.5. C. Etymology is the study of word origins. Semantics is about meaning, morphology is about word structure and syntax is about sentence structure.6. A. This famous line is from Hamlet.7. A. The sound /θ/ is produced by placing the tip of the tongue between the teeth.8. B. “blackboard” is made up of two words “black” and “board” and isa compound word.9. C. Benjamin Lee Whorf proposed the concept of “linguistic relativity” along with Edward Sapir.10. B. A sonnet typically has 14 lines.11. B. “can” is a modal verb which is used to express ability, permission etc.12. A. In “photograph” the stress is on the first syllable 'photograph.13. A. French has had the most influence on the development of Modern English, especially after the Norman Conquest.14. D. A catenative construction involves a verb followed by another verb in a non - finite form, here “made” followed by “clean”.15. A. Romanticism emphasized individualism and the beauty of nature.二、阅读理解1. The Angles, the Saxons and the Jutes invaded Britain in the 5th century AD.2. Most of the Celtic speakers were pushed west and north by the invaders - mainly into what is now Wales, Scotland and Ireland.3. The Angles came from "Englaland".4. Old English did not sound or look like English today. It was highly inflected and had different word forms for different functions in a sentence.5. It means that words changed their endings depending on their function in the sentence. For example, “stan” for nominative and “stane” for dative case of the word for “stone”.6. The Norman Conquest in 1066 brought the French language which had a major influence on English. French words were added to the English vocabulary.7. After the Norman Conquest, the ruling class spoke French and the common people spoke English.8. The Angles came from "Englaland" and their language was called "Englisc", from which the words "England" and "English" are derived.9. It has changed through invasions like the Germanic tribes in the 5th century and the Norman Conquest in 1066. It has added words from other languages, and has changed in terms of grammar, for example from being highly inflected in Old English.10. As mentioned before, the word for “stone” was “stan” in the nominati ve case (when it was the subject of the sentence), but “stane” in the dative case (when it was the indirect object).三、简答题1. A simile is a figure of speech that makes a comparison between two different things using “like” or “as”, for example “My heart is like a singing bird”. A metaphor makes a comparison without using these words, for example “The road is a ribbon of moonlight”. The simile is more explicit in its comparison, while the metaphor is more implicit and often creates a more vivid and imaginative connection.2. The Romantic literary movement had several main features. It emphasized emotion over reason. Writers focused on the individual and the individual's experience of the world. There was a great love for nature, seeing it as a source of inspiration, beauty and spiritual renewal. It also had an interest in the supernatural, the past and the exotic. There was a celebration of the imagination and a rejection of some of the strict rules of neoclassical literature.3. According to the nativist theory proposed by Noam Chomsky, children are born with an innate language acquisition device (LAD). This LAD allows children to have an in - built knowledge of the basic principles of language. They are able to acquire language quickly because they have this pre - wired system. They are exposed to the language in their environment and use the LAD to make sense of the input, formulating rules and gradually developing their language skills. Another theory, the behaviorist theory, proposed by Skinner, believes that language acquisition is a result of conditioning. Children learn language by imitating thelanguage they hear around them and are rewarded when they use language correctly.四、Essay QuestionEnglish has become a global language for several important reasons. Firstly, the history of British colonialism spread the language all over the world. Britain had colonies in many parts of the globe and as a result, English was introduced and became an important language in these areas. For example, in India, English is still widely used in education, business and government.Secondly, the United States, which is a superpower, has English as its main language. American influence in the fields of business, entertainment (Hollywood movies, popular music), technology and academia has made English even more widespread. People all over the world need to learn English to access American products, services and knowledge.In the international business world, English is the lingua franca. Multinational companies use English as their common language for communication. This allows people from different countries with different native languages to communicate effectively. For example, a Japanese and a Brazilian can communicate in English in a business meeting.In the field of science and technology, most research papers are published in English. Scientists need to know English to keep up with thelatest research findings and to share their own work. It is also the language of international conferences and seminars.In the field of education, many universities around the world offer courses in English. Students who want to study abroad or get a more international education often need to have a good command of English.However, the dominance of English also has some drawbacks. It can lead to the marginalization of other languages and cultures. But overall, the importance of English as a global language cannot be underestimated as it has become an essential tool for international communication, trade, knowledge sharing and cultural exchange.建议：嗨，同学！咱先来说说这试卷哈。

自然语言处理及计算语言学相关术语中英对译表二自然语言处理及计算语言学相关术语中英对译表二 delimiter 定界符号 [定界符]denotation 外延denotic logic 符号逻辑dependency 依存关系dependency gram r 依存关系语法dependency relation 依存关系depth-first search 深度优先搜寻derivation 派生derivational bound morpheme 派生性附着语素descriptive gram r 描述型语法 [描写语法]descriptive linguistics 描述语言学 [描写语言学] desiderative 意愿的determiner 限定词deterministic algorithm 决定型算法 [确定性算法] deterministic finite state auto ton 决定型有限状态机deterministic parser 决定型语法剖析器 [确定性句法剖析程序] developmental psychology 开展心理学diachronic linguistics 历时语言学diacritic 附加符号dialectology 方言学dictionary database 辞典数据库 [词点数据库]dictionary entry 辞典条目digital pro ssing 数字处理 [数值处理] diglossia 双言digraph 二合字母diminutive 指小词diphone 双连音directed acyclic graph 有向非循环图disambiguation 消除歧义 [歧义消除] discourse 篇章discourse ysis 篇章分析 [言谈分析] discourse planning 篇章规划discourse representation theory 篇章表征理论 [言谈表示理论] discourse strategy 言谈策略discourse structure 言谈结构discrete 离散的disjunction 选言dissimilation 异化distributed 分布式的distributed cooperative reasoning 分布协调型推理distributed text parsing 分布式文本剖析disyllabic 双音节的ditransitive verb 双宾动词 [双宾语动词;双及物动词]divergen 扩散[分化]d-m (determiner-measure) construction 定量结构d-n (determiner-noun) construction 定名结构document retrieval system 文件检索系统 [文献检索系统] do in dependency 领域依存性 [领域依存关系]double insertion 交互中插double-base 双基downgrading 降级dummy 虚位duration 音长{ 学}/时段{语法学/语意学}dynamic programming 动态规划earley algorithm earley 算法echo 回声句egressive 呼气音ejective 紧喉音electronic dictionary 电子词典elementary string 根本字符串 [根本单词串] ellipsis 省略em algorithm em算法embedding 崁入emic 功能关系的empirici 经验论empty category principle 虚范畴原那么 [空范畴原理] empty word 虚词enclitics 后接成份end user 终端用户 [最终用户]endo ntric 同心的endophora 语境照应entailment 蕴涵entity 实体entropy 熵entry 条目episodic memory 情节性记忆epistemological work 认识论网络ergative verb 作格动词ergativity 作格性esperando 世界语etic 无功能关系etymology 词源学eventevent driven control 驱动型控制example-based chine translation 以例句为本的机器翻译excla tion 感慨exclusive disjunction 排它性逻辑“或”experien r case 经验者格expert system 专家系统extension 外延external argument 域外论元extraposition 移外变形 [外置转换]facility value 易度值feature 特征feature bundle 特征束feature co-ourren restriction 特征同现限制 [特性同现限制] feature instantiation 特征表达feature structure 特征结构 [特性结构]feature unification 特征连并 [特性合一]feedback 回馈felicity condition 妥适条件file structure 档案结构finite auto ton 有限状态机 [有限自动机]finite state 有限状态finite state morphology 有限状态构词法 [有限状态词法] finite-state auto ta 有限状态自动机finite-state language 有限状态语言finite-state chine 有限状态机finite-state transdu r 有限状态置换器flap 闪音flat 降音foreground infor tion 前景讯息 [前景信息]for l language theory 形式语言理论for l linguistics 形式语言学for l se ntics 形式语意学forward inferen 前向推理 [向前推理]forward-backward algorithm 前前后后算法frame 框架frame based knowledge representation 框架型知识表示frame theory 框架理论free morpheme 自由语素fregean principle fregean 原那么fricative 擦音f-structure 功能结构full text searching 全文检索function word 功能词functional gram r 功能语法functional programming 函数型程序设计 [函数型程序设计] functional senten perspective 功能句子观functional structure 功能结构functional unification 功能连并 [功能合一]functor 功能符fundamental frequency 基频garden path senten 花园路径句gb (gover ent and binding) 管辖约束geminate 重叠音gender 性generalized phrase structure gram r 概化词组结构语法 [广义短语结构语法]generative gram r 衍生语法generative linguistics 衍生语言学 [生成语言学]generic 泛指geic epistemology 发生认识论geive rker 属格标记genitive 属格gerund 动名词gover ent and binding theory 管辖约束理论gpsg (generalized phrase structure gram r) 概化词组结构语法[广义短语结构语法]gradability 可分级性gram r checker 文法检查器gram tical affix 语法词缀gram tical category 语法范畴gram tical function 语能gram tical inferen 文法推论gram tical relation 语法关系grapheme 字素haplology 类音删略head 中心语head driven phrase structure 中心语驱动词组结构 [中心词驱动词组结构]head feature convention 中心语特征继承原理 [中心词特性继承原理]head-driven phrase structure gram r 中心语驱动词组结构律heteronym 同形heuristic parsing 经验式句法剖析heuristics 经验知识hidden rkov model 隐式马可夫模型hierarchical structure 阶层结构 [层次结构]holophrase 单词句homograph 同形异义词homonym 同音异义词homophone 同音词homophony 同音异义homorganic 同部位音的horn clause horn 子句hpsg (head-driven phrase structure gram r) 中心语驱动词组结构语法hu n- chine inte 人机界面hypernym 上位词hypertext 超文件 [超文本]hyponym 下位词hypotactic 主从结构的ic (immediate constituent) 直接成份icg (infor tion-based case gram r) 讯息为本的格位语法idiom 成语 [熟语]idiosyncrasy 特异性illocutionary 施为性immediate constituent 直接成份imperative 祈使句implicative predicate 蕴含谓词implicature 含意indexical 标引的indirect object 间接宾语indirect speech act 间接言谈行动 [间接言语行为] indo-european language 印欧语言inductional inferen 归纳推理inferen chine 推理机器infinitive 不定词 [to 不定式]infix 中缀inflection/inflexion 屈折变化inflectional affix 屈折词缀infor tion extraction 信息撷取infor tion pro ssing 信息处理 [信息处理]infor tion retrieval 信息检索infor tion scien 信息科学 [信息科学; 情报科学] infor tion theory 信息论 [信息论]inherent feature 固有特征inherit 继承inheritan 继承inheritan hierarchy 继承阶层 [继承层次]inheritan of attribute 属性继承innateness position 语法天生假说insertion 中插inside-outside algorithm 里里外外算法instantiation 表达instrumental (case) 工具格integrated parser 集成句法剖析程序integrated theory of discourse ysis 篇章分析综合理论 [言谈分析综合理论]in igen intensive production 知识密集型生产intensifier 加强成分intensional logic 内含逻辑intensional se ntics 内涵语意学intensional type 内含类型interjection/excla tion 感慨词inter-level 中间成分interlingua 中介语言interlingual 中介语(的）interlocutor 对话者internalise 内化international phoic association (ipa) 国际学会inter 网际网络interpretive se ntics 诠释性语意学intonation 语调intonation unit (iu) 语调单位ipa (international phoic association) 国际学会ir (infor tion retrieval) 信息检索is-a relation is-a 关系isomorphi 同形现象iu (intonation unit) 语调单位junction 连接keyword in context 上下文中关键词[上下文内关键词] kinesics 体势学knowledge acquisition 知识习得knowledge base 知识库knowledge based chine translation 知识为本之机器翻译knowledge extraction 知识撷取 [知识题取]knowledge representation 知识表示kwic (keyword in context) 关键词前后文 [上下文内关键词] label 卷标labial 唇音labio-dental 唇齿音labio-velar 软颚唇音lad (language acquisition devi ) 语言习得装置lag 发声延迟language acquisition 语言习得language acquisition devi 语言习得装置language engineering 语言工程language generation 语言生成language intuition 语感language model 语言模型language technology 语言科技left-corner parsing 左角落剖析 [左角句法剖析] lem 词元lenis 弱辅音letter-to-phone 字转音lexeme 词汇单位lexical ambiguity 词汇歧义lexical category 词类lexical con ptual structure 词汇概念结构lexical entry 词项lexical entry selection standard 选词标准lexical integrity 词语完整性lexical se ntics 词汇语意学lexical-functional gram r 词汇功能语法lexicography 词典学lexicology 词汇学lexicon 词汇库 [词典;词库]lexis 词汇层lf (logical form) 逻辑形式lfg (lexical-functional gram r) 词汇功能语法liaison 连音linear bounded auto ton 线性有限自主机linear pre den 线性次序lingua franca 共通语linguistic decoding 语言译码linguistic unit 语言单位linked list 串行loan 外来语local 局部的locali 方位主义localizer 方位词locus model 轨迹模型locution 惯用语logic 逻辑logic array work 逻辑数组网络logic programming 逻辑程序设计 [逻辑程序设计] logical form 逻辑形式logical operator 逻辑算子 [逻辑算符]logic-based gram r 逻辑为本语法 [基于逻辑的语法] long term memory 记忆longest tch principle 最长匹配原那么 [最长一致法] lr (left-right) parsing lr 剖析chine dictionary 机器词典chine language 机器语言chine learning 机器学习chine translation 机器翻译chine-readable dictionary (mrd) 机读辞典crolinguistics 宏观语言学rkov chart 马可夫图the tical linguistics 数理语言学ximum entropy 最大熵m-d (modifier-head) construction 偏正结构mean length of utteran (mlu) 语句平均长度measure of infor tion 讯习测度 [信息测度] memory based 根据记忆的mental lexicon 心理词汇库mental model 心理模型mental pro ss 心理过程 [智力过程;智力处理] metalanguage 超语言metaphor 隐喻metaphorical extension 隐喻扩展metarule 律上律 [元规那么]metathesis 易位microlinguistics 微观语言学middle structure 中间式结构mini l pair 最小对mini list program 微言主义mlu (mean length of utteran ) 语句平均长度modal 情态词modal auxiliary 情态助动词modal logic 情态逻辑modifier 修饰语modular logic gram r 模块化逻辑语法modular parsing system 模块化句法剖析系统modularity 模块性(理论)module 模块monophthong 单元音monotonic 单调monotonicity 单调性montague gram r 蒙泰究语法 [蒙塔格语法] mood 语气morpheme 词素morphological affix 构词词缀morphological deposition 语素分解morphological pattern 词型morphological pro ssing 词素处理morphological rule 构词律 [词法规那么] morphological segmentation 语素切分morphology 构词学morphophonemics 词音学 [形态音位学;语素音位学] morphophonological rule 形态音位规那么morphosyntax 词句法motor theory 肌动理论movement 移位mrd ( chine-readable dictionary) 机读辞典模板,内容仅供参考。

由安博测试空间技术中心提供软件测试英语单词Acceptance testing : 验收测试Acceptance Testing：可接受性测试Accessibility test : 软体适用性测试actual outcome：实际结果Ad hoc testing : 随机测试Algorithm analysis : 算法分析algorithm：算法Alpha testing : α测试analysis：分析anomaly：异常application software：应用软件Application under test (AUT) : 所测试的应用程序Architecture : 构架Artifact : 工件ASQ：自动化软件质量（Automated Software Quality）Assertion checking : 断言检查Association : 关联Audit : 审计audit trail：审计跟踪Automated Testing：自动化测试Backus-Naur Form：BNF范式baseline：基线Basic Block：基本块basis test set：基本测试集Behaviour : 行为Bench test : 基准测试benchmark：标杆/指标/基准Best practise : 最佳实践Beta testing : β测试Black Box Testing：黑盒测试Blocking bug : 阻碍性错误Bottom-up testing : 自底向上测试boundary value coverage：边界值覆盖boundary value testing：边界值测试Boundary values : 边界值Boundry Value Analysis：边界值分析branch condition combination coverage：分支条件组合覆盖branch condition combination testing：分支条件组合测试branch condition coverage：分支条件覆盖branch condition testing：分支条件测试branch condition：分支条件Branch coverage : 分支覆盖branch outcome：分支结果branch point：分支点branch testing：分支测试branch：分支Breadth Testing：广度测试Brute force testing: 强力测试Buddy test : 合伙测试Buffer : 缓冲Bug : 错误Bug bash : 错误大扫除bug fix : 错误修正Bug report : 错误报告Bug tracking system: 错误跟踪系统bug：缺陷Build : 工作版本（内部小版本）Build Verfication tests(BVTs): 版本验证测试Build-in : 内置Capability Maturity Model (CMM): 能力成熟度模型Capability Maturity Model Integration (CMMI): 能力成熟度模型整合capture/playback tool：捕获/回放工具Capture/Replay Tool：捕获/回放工具CASE：计算机辅助软件工程（computer aided software engineering）CAST：计算机辅助测试cause-effect graph：因果图certification ：证明change control：变更控制Change Management :变更管理Change Request :变更请求Character Set : 字符集Check In :检入Check Out :检出Closeout : 收尾code audit ：代码审计Code coverage : 代码覆盖Code Inspection：代码检视Code page : 代码页Code rule : 编码规范Code sytle : 编码风格Code Walkthrough：代码走读code-based testing：基于代码的测试coding standards：编程规范Common sense : 常识Compatibility Testing：兼容性测试complete path testing ：完全路径测试completeness：完整性complexity ：复杂性Component testing : 组件测试Component：组件computation data use：计算数据使用computer system security：计算机系统安全性Concurrency user : 并发用户Condition coverage : 条件覆盖condition coverage：条件覆盖condition outcome：条件结果condition：条件configuration control：配置控制Configuration item : 配置项configuration management：配置管理Configuration testing : 配置测试conformance criterion：一致性标准Conformance Testing：一致性测试consistency ：一致性consistency checker：一致性检查器Control flow graph : 控制流程图control flow graph：控制流图control flow：控制流conversion testing：转换测试Core team : 核心小组corrective maintenance：故障检修correctness ：正确性coverage ：覆盖率coverage item：覆盖项crash：崩溃criticality analysis：关键性分析criticality：关键性CRM(change request management): 变更需求管理Customer-focused mindset : 客户为中心的理念体系Cyclomatic complexity : 圈复杂度data corruption：数据污染data definition C-use pair：数据定义C-use使用对data definition P-use coverage：数据定义P-use覆盖data definition P-use pair：数据定义P-use使用对data definition：数据定义data definition-use coverage：数据定义使用覆盖data definition-use pair ：数据定义使用对data definition-use testing：数据定义使用测试data dictionary：数据字典Data Flow Analysis : 数据流分析data flow analysis：数据流分析data flow coverage：数据流覆盖data flow diagram：数据流图data flow testing：数据流测试data integrity：数据完整性data use：数据使用data validation：数据确认dead code：死代码Debug : 调试Debugging：调试Decision condition：判定条件Decision coverage : 判定覆盖decision coverage：判定覆盖decision outcome：判定结果decision table：判定表decision：判定Defect : 缺陷defect density : 缺陷密度Defect Tracking :缺陷跟踪Deployment : 部署Depth Testing：深度测试design for sustainability :可延续性的设计design of experiments：实验设计design-based testing：基于设计的测试Desk checking : 桌前检查desk checking：桌面检查Determine Usage Model : 确定应用模型Determine Potential Risks : 确定潜在风险diagnostic：诊断DIF(decimation in frequency) : 按频率抽取dirty testing：肮脏测试disaster recovery：灾难恢复DIT （decimation in time）: 按时间抽取documentation testing ：文档测试domain testing：域测试domain：域DTP DETAIL TEST PLAN详细确认测试计划Dynamic analysis : 动态分析dynamic analysis：动态分析Dynamic Testing：动态测试embedded software：嵌入式软件emulator：仿真End-to-End testing：端到端测试Enhanced Request :增强请求entity relationship diagram：实体关系图Encryption Source Code Base：加密算法源代码库Entry criteria : 准入条件entry point ：入口点Envisioning Phase : 构想阶段Equivalence class : 等价类Equivalence Class：等价类equivalence partition coverage：等价划分覆盖Equivalence partition testing : 等价划分测试equivalence partition testing:参考等价划分测试equivalence partition testing：等价划分测试Equivalence Partitioning：等价划分Error : 错误Error guessing : 错误猜测error seeding：错误播种/错误插值error：错误Event-driven : 事件驱动Exception handlers : 异常处理器exception：异常/例外executable statement：可执行语句Exhaustive Testing：穷尽测试exit point：出口点expected outcome：期望结果Exploratory testing : 探索性测试Failure : 失效Fault : 故障fault：故障feasible path：可达路径feature testing：特性测试Field testing : 现场测试FMEA：失效模型效果分析（Failure Modes and Effects Analysis）FMECA：失效模型效果关键性分析(Failure Modes and Effects Criticality Analysis)Framework : 框架FTA：故障树分析(Fault Tree Analysis)functional decomposition：功能分解Functional Specification ：功能规格说明书Functional testing : 功能测试Functional Testing：功能测试G11N(Globalization) : 全球化Gap analysis : 差距分析Garbage characters : 乱码字符glass box testing：玻璃盒测试Glass-box testing : 白箱测试或白盒测试Glossary : 术语表GUI(Graphical User Interface): 图形用户界面Hard-coding : 硬编码Hotfix : 热补丁I18N(Internationalization): 国际化Identify Exploratory Tests –识别探索性测试IEEE：美国电子与电器工程师学会（Institute of Electrical and Electronic Engineers）Incident 事故Incremental testing : 渐增测试incremental testing：渐增测试infeasible path：不可达路径input domain：输入域Inspection : 审查inspection：检视installability testing：可安装性测试Installing testing : 安装测试instrumentation：插装instrumenter：插装器Integration :集成Integration testing : 集成测试interface : 接口interface analysis：接口分析interface testing：接口测试interface：接口invalid inputs：无效输入isolation testing：孤立测试Issue : 问题Iteration : 迭代Iterative development: 迭代开发job control language：工作控制语言Job：工作Key concepts : 关键概念Key Process Area : 关键过程区域Keyword driven testing : 关键字驱动测试Kick-off meeting : 动会议L10N(Localization) : 本地化Lag time : 延迟时间LCSAJ：线性代码顺序和跳转（Linear Code Sequence And Jump）LCSAJ coverage：LCSAJ覆盖LCSAJ testing：LCSAJ测试Lead time : 前置时间Load testing : 负载测试Load Testing：负载测试Localizability testing: 本地化能力测试Localization testing : 本地化测试logic analysis：逻辑分析logic-coverage testing：逻辑覆盖测试Maintainability : 可维护性maintainability testing：可维护性测试Maintenance : 维护Master project schedule :总体项目方案Measurement : 度量Memory leak : 内存泄漏Migration testing : 迁移测试Milestone : 里程碑Mock up : 模型，原型modified condition/decision coverage：修改条件/判定覆盖modified condition/decision testing ：修改条件/判定测试modular decomposition:参考模块分解Module testing : 模块测试Monkey testing : 跳跃式测试Monkey Testing：跳跃式测试mouse over：鼠标在对象之上mouse leave：鼠标离开对象MTBF：平均失效间隔实际（mean time between failures）MTP MAIN TEST PLAN主确认计划MTTF：平均失效时间（mean time to failure）MTTR：平均修复时间（mean time to repair）multiple condition coverage：多条件覆盖mutation analysis：变体分析N/A(Not applicable) : 不适用的Negative Testing : 逆向测试, 反向测试, 负面测试negative testing:参考负面测试Negative Testing：逆向测试/反向测试/负面测试off by one：缓冲溢出错误non-functional requirements testing:非功能需求测试nominal load:额定负载N-switch coverage：N切换覆盖N-switch testing：N切换测试N-transitions：N转换Off-the-shelf software : 套装软件operational testing：可操作性测试output domain：输出域paper audit:书面审计Pair Programming : 成对编程partition testing：分类测试Path coverage : 路径覆盖path coverage：路径覆盖path sensitizing：路径敏感性path testing：路径测试path：路径Peer review : 同行评审Performance : 性能Performance indicator: 性能（绩效）指标Performance testing : 性能测试Pilot : 试验Pilot testing : 引导测试Portability : 可移植性portability testing：可移植性测试Positive testing : 正向测试Postcondition : 后置条件Precondition : 前提条件precondition：预置条件predicate data use：谓词数据使用predicate：谓词Priority : 优先权program instrumenter：程序插装progressive testing：递进测试Prototype : 原型Pseudo code : 伪代码pseudo-localization testing：伪本地化测试pseudo-random：伪随机QC：质量控制（quality control）Quality assurance(QA): 质量保证Quality Control(QC) : 质量控制Race Condition：竞争状态Rational Unified Process(以下简称RUP):瑞理统一工艺Recovery testing : 恢复测试recovery testing：恢复性测试Refactoring : 重构regression analysis and testing：回归分析和测试Regression testing : 回归测试Release : 发布Release note : 版本说明release：发布Reliability : 可靠性reliability assessment：可靠性评价reliability：可靠性Requirements management tool: 需求管理工具Requirements-based testing : 基于需求的测试Return of Investment（ROI）: 投资回报率review：评审Risk assessment : 风险评估risk：风险Robustness : 强健性Root Cause Analysis(RCA): 根本原因分析safety critical：严格的安全性safety：（生命）安全性Sanity testing : 健全测试Sanity Testing：理智测试Schema Repository : 模式库Screen shot : 抓屏、截图SDP：软件开发计划（software development plan）Security testing : 安全性测试security testing：安全性测试security.：（信息）安全性serviceability testing：可服务性测试Severity : 严重性Shipment : 发布simple subpath：简单子路径Simulation : 模拟Simulator : 模拟器SLA(Service level agreement): 服务级别协议SLA：服务级别协议（service level agreement）Smoke testing : 冒烟测试Software development plan(SDP): 软件开发计划Software development process: 软件开发过程software development process：软件开发过程software diversity：软件多样性software element：软件元素software engineering environment：软件工程环境software engineering：软件工程Software life cycle : 软件生命周期source code：源代码source statement：源语句Specification : 规格说明书specified input：指定的输入spiral model ：螺旋模型SQAP SOFTWARE QUALITY ASSURENCE PLAN 软件质量保证计划SQL：结构化查询语句（structured query language）Staged Delivery：分布交付方法state diagram：状态图state transition testing ：状态转换测试state transition：状态转换state：状态Statement coverage : 语句覆盖statement testing：语句测试statement：语句Static Analysis：静态分析Static Analyzer：静态分析器Static Testing：静态测试statistical testing：统计测试Stepwise refinement : 逐步优化storage testing：存储测试Stress Testing : 压力测试structural coverage：结构化覆盖structural test case design：结构化测试用例设计structural testing：结构化测试structured basis testing：结构化的基础测试structured design：结构化设计structured programming：结构化编程structured walkthrough：结构化走读stub：桩sub-area：子域Summary：总结SVVP SOFTWARE Vevification&Validation PLAN：软件验证和确认计划symbolic evaluation：符号评价symbolic execution:参考符号执行symbolic execution：符号执行symbolic trace：符号轨迹Synchronization : 同步Syntax testing : 语法分析system analysis：系统分析System design : 系统设计system integration：系统集成System Testing : 系统测试TC TEST CASE 测试用例TCS TEST CASE SPECIFICATION 测试用例规格说明TDS TEST DESIGN SPECIFICATION 测试设计规格说明书technical requirements testing：技术需求测试Test : 测试test automation：测试自动化Test case : 测试用例test case design technique：测试用例设计技术test case suite：测试用例套test comparator：测试比较器test completion criterion：测试完成标准test coverage:测试覆盖Test design : 测试设计Test driver : 测试驱动test environment:测试环境test execution technique:测试执行技术test execution:测试执行test generator:测试生成器test harness:测试用具Test infrastructure : 测试基础建设test log:测试日志test measurement technique:测试度量技术Test Metrics :测试度量test procedure:测试规程test records:测试记录test report:测试报告Test scenario : 测试场景Test Script:测试脚本Test Specification:测试规格Test strategy : 测试策略test suite:测试套Test target : 测试目标Test ware : 测试工具Testability : 可测试性testability:可测试性Testing bed : 测试平台Testing coverage : 测试覆盖Testing environment : 测试环境Testing item : 测试项Testing plan : 测试计划Testing procedure : 测试过程Thread testing : 线程测试time sharing:时间共享time-boxed : 固定时间TIR test incident report 测试事故报告ToolTip:控件提示或说明top-down testing:自顶向下测试TPS TEST PEOCESS SPECIFICATION 测试步骤规格说明Traceability : 可跟踪性traceability analysis:跟踪性分析traceability matrix:跟踪矩阵Trade-off : 平衡transaction:事务/处理transaction volume：交易量transform analysis:事务分析trojan horse:特洛伊木马truth table:真值表TST TEST SUMMARY REPORT 测试总结报告Tune System : 调试系统TW TEST WARE :测试件Unit Testing :单元测试Usability Testing:可用性测试Usage scenario : 使用场景User acceptance Test : 用户验收测试User database :用户数据库User interface(UI) : 用户界面User profile : 用户信息User scenario : 用户场景V&V (Verification & Validation) : 验证&确认validation :确认verification :验证version :版本Virtual user : 虚拟用户volume testing:容量测试VSS（visual source safe）：VTP Verification TEST PLAN验证测试计划VTR Verification TEST REPORT验证测试报告Walkthrough : 走读Waterfall model : 瀑布模型Web testing : 网站测试White box testing : 白盒测试Work breakdown structure (WBS) : 任务分解结构Zero bug bounce (ZBB) : 零错误反弹由安博测试空间技术中心提供一、对软件测试的误解1. 如果发布出去的软件有质量问题,那是软件测试人员的错.2. 软件测试技术要求不高,至少比编程容易多了3. 软件测试随便找一个能力差的人就能做.4. 软件测试是测试人员的事,与开发人员无关.5. 设计-实现-测试,软件测试是开发后期的一个阶段二、如何理解软件测试软件测试是一种有效的提高软件质量的手段,但即使在投入上有所保证,测试也不能百分为百发现所有质量隐患.况且软件质量并不仅仅是测试出来的.很多人认为软件测试就是运行一下软件,看看结果对不对.但实际上,如何在有限的投入下,提高软件测试的效率和产出是一件很见功底的事.好的测试人员不仅要掌握各种测试技术,还要具备丰富的编程经验和对BUG的敏感.测试的复杂之处,除了测试技术问题之外,还有测试管理问题.测试不是可有可无,随心所欲的.规范化的软件开发需要对软件测试早做计划,分配必要的时间,人力和财力等资源,并将其作为项目管理的一个部分加以控制和协调. 开发和测试是软件项目相辅相成的两个过程,人员间的交流,协作和配合是提高整体效率的重要因素.软件产品开发完毕,再进行测试的观念是有悖于生命周期理论的.软件产品质量问题越晚发现,修复的代价越大.一些常识和经验之谈测试能提高软件的质量，但是提高质量不能依赖测试。

The Differences Between Chinese And Western – Language and CultureName & ID: 周煜201032029郭琪201032108李秋风201032096郭启帆201032107刘星延201032002Major: International BusinessAbstract:In different philosophy, cultural background of the formation of a different ways of thinking of different nationalities, different modes of thinking and the language at the structural level difference, and are reflected in the language and the solidification. This report focuses on two aspects about The mode of thinking and structure level.Key words:way of thinking, structure level, rationalism, linear thinking pattern. ,streamline the thoughts.1 IntroductionChinese culture holds that external nature is a whole, not analysis, can not explain, can feel, experience, insight and understanding.Although there is a certain status in epistemology, but not based on rigorous analysis based on scientific proof, so can only be rough general and vague, with no great accuracy.This insight, implicit philosophical and religious thought and Chinese, especially the fuzziness in classical Chinese come down in one continuous line.Western rationalism, western thinkers calmly abide by their own point of view and the way. Their study on the whole scientific system to be thorough in the full range of independent thinking. Western philosophy emphasizes analysis, highlighting the formal logic. Aristotle founded the deductive reasoning, inductive reasoning proposed by Bacon is a powerful evidence2 Culture reflect on languageChinese love taking person as subject: I, you, he (she, it), we, you, they. Some sentences form seemingly no subject, but in fact it is the omitted subject, the subject is still a human being. If there is no subject, sometimes simply use no subject, such as "rain", also refused to use as the subject.English is different, English common objects as subject, with the impersonal sentence (inpersonal), based on the objective stated objective facts. According to statistics, there are 50% English sentences of the subject of the sentence is an abstract noun, impersonal things name as "it", "there (be)" and other non personal pronoun. Such as:Curiosity drew me to open the box.The year of 1949 saw the founding of the PRC.It takes an hour to get there of foot.There has been great changes since the opening up.3The overall VS individualChinese towards things, pay attention to overall, from one thing and he relations of things to understand, to solve.Western culture has distinct characteristics of the individual.4 Two languages in grammar is differentMorphological changes of Chinese grammar is not a strict sense, the word order is relatively fixed, the main, predicate, object, complement, shape, cannot exchange.While English is much more flexible than. Through morphological changes (inflection) change the part of speech, word order sentences change, flexible, expression of an almost identical.For example, "many Chinese students in this big and bright Reading Library" say:A lot of students are reading in this big and bright library.A lot of students are reading in this library which is big and bright.There are a lot of students reading in this big and bright library.This big and bright library seat a lot of students who are reading now.5 Cultural language the different ways of thinking - the main VS objectSeeking unification mode of thinking China traditional ancient philosopher satisfied by intuition to get an overall impression in the understanding of objective things, but this intuition is the subject of human. The culture and thinking of the China by people as the starting point, the foothold, emphasizes human value, significance, seeking truth, emphasize ethics.Western traditional philosophy about "one divides into two", man and nature to the opposite, and tries to find the objective law, is the study of the relationship between man and nature. Western philosophers pay attention to object, pay attention to the understanding and study of the objective world. Reflected in the language: Chinese love taking person as subject: I, you, he (she, it), we, you, they. Some sentences form seemingly no subject, but in fact it is the omitted subject, the subject is still a human being. If there is no subject, sometimes simply use no subject, such as "rain", also refused to use as the subject.English is different, English common objects as subject, with the impersonal sentence (inpersonal), based on the objective stated objective facts. According to statistics, there are 50% English sentences of the subject of the sentence is an abstract noun, impersonal things name as "it", "there (be)" and other non personal pronoun. Such as:Curiosity drew me to open the box.The year of 1949 saw the founding of the PRC.It takes an hour to get there of foot.There has been great changes since the opening up.English passive voice (passive voice) is not only not move 'case, but also for syntactic, rhetoric, style and genre considerations. For example, in order to highlight the objectivity, reality, news reports or papers in English more than a passive sentence;The opposition announced a boycott and clashes were reported across the country.While Chinese is quite different, in the report or thesis common "we must", "people should" wording, Chinese also use passive sentences, but in the authentic Chinese passive sentence is still prominent, the execution of the action, which is "......" By the word structure.Circulating VS linearSpiral curve Chinese traditional thinking pattern that has the characteristics of culture and thinking China follow, imitate, repeat. This cycle repeated the China habit thoughts of ancient culture and ideology has a strong affinity and stability of a connected, but in a sense also hindered the thinking extension, caused the Chinese sentences are short, loose structure, and the structure of complex roundabout, repeated.Western thinkers, originality and transcendence determines the mode of thinking of radial line structure (linear thinking pattern). They ultimately, pay attention to continuous development, avoid procrastination repeatedly.Each process is commonly used Chinese sentences clause sentences layer narrative thinking (streamline the thoughts), and word order is generally in terms of time and logic order, attributive modification front, a word can bear the modifier Co., a sentence in general to highlight a problem, which makes the Chinese word length in 7 to 12 words is the best, but also a unique language form four lattice. Because of its mode of thinking tends to be Multi Pocket some circles, Chinese article normal is - bearing - to -, often around the issues around in circles.The most obvious point is the English complex (complex). English long sentences, like a chain, showing a "architectural style of buildings" (architecture style). English sentence is the sentence first closed, open and China Chinese sentence; sentence open, end systolic different. A sentence by word order and arrange, indicates the relationship and connection means, plus a variety of parallel composition, additives, modifiers, clause complex clauses, extension of the continuous development, move forward, constantly changing like thinking, so in theory, an English sentence is endless.For example, I gave him the book. such a simple sentence can add many clauses in the suffix and the endless.Such as: I gave him the book which I bought in that store which was on the 21th Street where the traffic accident happened the ot her day when I went to visit my teacher who...In Chinese, "I gave the book to him" has become an independent sentence, if the narrative, is another one or several sentences task.From the textual perspective, because English Modes of thinking is the premise and minor premise - conclusion so thorough development, the article also beginning, middle end, emphasize the structure before and after the undertaking, straight into the centre.Research on modern brain science confirms, two hemispheres of the division of labor is different. The right hemisphere mainly deal with a variety of image processing, the left hemisphere is language symbol of every hue. This shows that the two left and right hemisphere thinking tool is different, the main tools for thinking the right hemisphere is the image, we can call this kind of thinking is the thinking in images; the main thinking tools of the left hemisphere is language, we can call this kind of thinking is the language of thinking. Language is the image of the symbol, image is representative of the significance of language. In the brain, between image and language, thinking and language thinking and not be indifferent to. On the contrary, the callosal connections of the two hemispheres of the brain in order to imagine the propagation velocity of left and right brain information.People often say, Chinese and Westerners have different ways of thinking. This is without a doubt. However, how are the different? This difference is how form?A variety of reasons.But I think, the differences between Chinese and Western writing, is the root cause of the two different ways of thinking. Of course, the text is written symbol language, which is different from the language, is not equal to the thinking tool. But as the people most often used communication tools, the text has not underestimate the impact of thinking. The written form of language is the alphabet text, this text does not form, not only ideographic, phonetic; that is to say, its direct connection completely cut off and the image, is a pure symbol of language. The pure record language alphabet text frequently, widely stimulated people's brain, gradually formed the westerners is longer than the language of thinking, the language thinking developed. While Chinese writing is one of Chinese characters, it not only sound, but also the pictographic, ideographic. The sound, shape, meaning connected text, providing a convenient tool for thinking in images, so that Chinese longer than the image thinking.Text effects of mode of thinking, ways of thinking and affect the development of culture. Chinese and Western languages and the different ways of thinking, the Chinese and Western culture showed a unique style. The western scholars think, language and thinking are interdependent. As Hagel said: "the thought form first and recorded in the human language." Dewey also pointed out: "we predicate thinking without language is not self storage." Linguistics textbook we are repeatedly stressed, language and thinking is the relationship between shell and kernel. On the contrary, many Chinese scholars think it is unable with the language to express the highest level of his thoughts.Such as "road to road, very road; a name, very name" (chapter this "me"), "speech, the coarse; can intends to send, the essence also" ("Chuang-tzu eyes," I "), meaning" ("book of changes on the copulative"), "without a word, as had the wind" ("poem, implicit") etc..Chinese and Western differences in thinking and language relationship, directly affect their linguistic interest. In order to better development, to improve their ability of thinking, Westerners have long attached great importance to the study of language. From the ancient Greece period, linguistics "into the 'humanities' and' science 'is a independent discipline", to modern, western linguistics has been be way ahead. And Chinese thinking on language is small, the corresponding to the study of language, Chinese less attention. There's been no independent development in the Chinese ancient linguistics. Confucius long advocated: "expressiveness." ("Analects of Confucius" the Duke) phonology is literature and classics client, people just to write poetry and article to study it. Scholars and even the text, phonology, exegesis is called the "primary school". Until the end of nineteenth Century, Ma Jianzhong just copy the western theory of language, written Chinese first grammar "Ma Shiwen.". Since then, Chinese linguistics was gradually developed independently.The different characteristics of Chinese and Western thought, but also a profound impact on the different temperament of Chinese and Western culture. Chinese philosophy and history of the three major schools of Confucianism and Buddhism have emphasized the reflection, experience and Enlightenment heart. The Confucianism has had said: "I daily reflect on oneself three times a day (with the book" Analects of Confucius "and" the), to reflect the essential means for self-cultivation. Taoism is a step further. Wang Bi said: "I like, but proud; forget the prophet, is like also. Pride in forgetting image, like in the forgotten." ("Book slightly cases of Ming as") language, even image have become bound ideological shackles, ideological cultivation reached a certain degree, image and language does not exist.The traditional point to reach the peak of perfection in the buddhists. Huineng although not words, but to promote "Epiphany" became the ancestor of Zen sect. Later, Zen simply that "by means of non-literature", completely abandon the language, complete with pure intuition transfer those considered the inexpressible secret, "freedom" is one of the main forms of. Therefore, the Buddhism developed in Chinese, Zen is in Chinese, Chinese thinking in images of soil is a reason not to be ignored. Corresponding to this, the concept of a series of mysterious formed in Chinese academic history, such as Yin and Yang, Qi, artistic conception, character, charm, and...... Too numerous to mention.In the language of thinking under the influence of western culture and western philosophy, show another style. Western philosophers are always close to the language and thought of kyo. The ancient Greek philosophers were so, so also the modern western philosophers. Therefore, in asense, the western philosophy is a kind of speculative philosophy of language. Of course, the concept of western academic history is quite clear.Experts think, thinking in images is fuzzy, it is characteristic of Chinese thinking; relatively speaking, language thinking with accuracy, which is characteristic of Western thinking. The different characteristics of Chinese and Western thinking, in their own language system have left their marks though, this same Chinese and Westerners to language study different attitudes also have a certain relationship.That is to say, the western language is accurate, the Chinese, especially in ancient Chinese is relatively vague (due to the large number of western translation of the input, the modern Chinese are to the precise development). The same meaning, Nakanishi Tetsuhito expression styles. Such as me said: "there are no together accrue, phase easily also, the length of phase, phase interference they also, Aiwa Ya sound, it follows." (abridged edition "me" second parts and ninth chapters) similar meaning in Heraclitus there has become a "unified material is composed of two opposite composition, so it is divided into two halves, the two opposite will be revealed." Confucius definition of wisdom: "know what one really understands, admit what you don't know, is know." ("the Analects of Confucius for the government") Aristotle said: "wisdom is about certain principles and causes of knowledge." [4] although the Heraclitus and Aristotle words translated into modern Chinese and its accuracy is not lost; but me and Confucius quotations must pass a grasp can get the truth.From the above comparison, we can find, on the surface, the ancient Greek philosopher of language is abstract, general bright, and Chinese sages of the language has the prominent representation, figurative. But this is not to say that Chinese lack of abstract thinking. In fact, in this embodiment, figurative behind, but the expression with Western philosopher of the same abstract reasoning.So, some people think that western thinking is abstract, Chinese lack of abstract thinking, this is an illusion. Who can say "meaning grasped imageries forgotten" is not an abstract? Who can say "heart", "identity" is not an abstract? But they are whirling, difficult to express. Even the normally demote Chinese philosophy, Haggle had to admit, "book of changes" in "the graphic meaning is extremely abstract category, is a purely rational regulations."For a long time people to abstract thinking (specifically the language thinking) and logical thinking be confused, so that Chinese thinking lack of abstract person, often also asserted that Chinese thinking lack of logic. This is the same illusion. The so-called logic, is the objective law of the. In fact, reflect the objective laws of thinking is the logical thinking; image thinking but also reflects the objective law, of course, is also a kind of logical thinking.Of course, we do not deny that, abstract, logical thinking and image thinking language have different characteristics. Abstract logical thinking, la. Abstract logical thinking, language in the language, obviously in the language, so is the external; abstract, logic of thinking in image in the image, in the language expression is not so obvious, so it is potential. This is the root cause of the above all kinds of illusion.。

inferenceInference is the act of drawing a conclusion by deductive reasoning from given facts. The conclusion drawn is also called an inference. The laws of valid inference are studied in the field of logic.Human inference (i.e. how humans draw conclusions) is traditionally studied within the field of cognitive psychology; artificial intelligence researchers develop automated inference systems to emulate human inference. Statistical inference allows for inference from quantitative data.Contents[hide]1 Accuracy of inductive inferences2 Examples of deductive inference3 Incorrect inference4 Automatic logical inferenceo 4.1 Example using Prologo 4.2 Use with the semantic webo 4.3 Bayesian statistics and probability logico 4.4 Nonmonotonic logic[1]5 See also6 References[edit] Accuracy of inductive inferencesThe process by which a conclusion is inferred from multiple observations is called inductive reasoning. The conclusion may be correct or incorrect, or correct to within a certain degree of accuracy, or correct in certain situations. Conclusions inferred from multiple observations may be tested by additional observations.[edit] Examples of deductive inferenceGreek philosophers defined a number of syllogisms, correct three part inferences, that can be used as building blocks for more complex reasoning. We begin with the most famous of them all:1.All men are mortal2.Socrates is a man3.Therefore, Socrates is mortal.The reader can check that the premises and conclusion are true, but Logic is concerned with inference: does the truth of the conclusion follow from that of the premises?The validity of an inference depends on the form of the inference. That is, the word "valid" does not refer to the truth of the premises or the conclusion, but rather to the form of the inference. An inference can be valid even if the parts are false, and can be invalid even if the parts are true. But a valid form with true premises will always have a true conclusion.For example, consider the form of the following symbological track:1.All apples are blue.2. A banana is an apple.3.Therefore, a banana is blue.For the conclusion to be necessarily true, the premises need to be true.Now we turn to an invalid form.1.All A are B.2. C is a B.3.Therefore, C is an A.To show that this form is invalid, we demonstrate how it can lead from true premises to a false conclusion.1.All apples are fruit. (True)2.Bananas are fruit. (True)3.Therefore, bananas are apples. (False)A valid argument with false premises may lead to a false conclusion:1.All fat people are Greek.2.John Lennon was fat.3.Therefore, John Lennon was Greek.When a valid argument is used to derive a false conclusion from false premises, the inference is valid because it follows the form of a correct inference.A valid argument can also be used to derive a true conclusion from false premises:1.All fat people are musicians2.John Lennon was fat3.Therefore, John Lennon was a musicianIn this case we have two false premises that imply a true conclusion.[edit] Incorrect inferenceAn incorrect inference is known as a fallacy. Philosophers who study informal logic have compiled large lists of them, and cognitive psychologists have documented many biases in human reasoning that favor incorrect reasoning.[edit] Automatic logical inferenceAI systems first provided automated logical inference and these were once extremely popular research topics, leading to industrial applications under the form of expert systems and later business rule engines.An inference system's job is to extend a knowledge base automatically. The knowledge base (KB) is a set of propositions that represent what the system knows about the world. Several techniques can be used by that system to extend KB by means of valid inferences. An additional requirement is that the conclusions the system arrives at are relevant to its task.[edit] Example using PrologProlog (for "Programming in Logic") is a programming language based on a subset of predicate calculus. Its main job is to check whether a certain proposition can be inferred from a KB (knowledge base) using an algorithm called backward chaining.Let us return to our Socrates syllogism. We enter into our Knowledge Base the following piece of code:mortal(X) :- man(X).man(socrates).( Here :-can be read as if. Generally, if P Q(if P then Q) then in Prolog we would code Q:-P (Q if P).)This states that all men are mortal and that Socrates is a man. Now we can ask the Prolog system about Socrates:- mortal(socrates).(where ?- signifies a query: Can mortal(socrates). be deduced from the KB using the rules) gives the answer "Yes".On the other hand, asking the Prolog system the following:- mortal(plato).gives the answer "No".This is because Prolog does not know anything about Plato, and hence defaults to any property about Plato being false (the so-called closed world assumption). Finally ?- mortal(X) (Is anything mortal) would result in "Yes" (and in some implementations: "Yes": X=socrates)Prolog can be used for vastly more complicated inference tasks. See the corresponding article for further examples. [edit] Use with the semantic webRecently automatic reasoners found in semantic web a new field of application. Being based upon first-order logic, knowledge expressed using one variant of OWL can be logically processed, i.e., inferences can be made upon it.[edit] Bayesian statistics and probability logicPhilosophers and scientists who follow the Bayesian framework for inference use the mathematical rules of probability to find this best explanation. The Bayesian view has a number of desirable features—one of them is that it embeds deductive (certain) logic as a subset (this prompts some writers to call Bayesian probability "probability logic", following E. T. Jaynes). Bayesians identify probabilities with degrees of beliefs, with certainly true propositions having probability 1, and certainly false propositions having probability 0. To say that "it's going to rain tomorrow" has a 0.9 probability is to say that you consider the possibility of rain tomorrow as extremely likely.Through the rules of probability, the probability of a conclusion and of alternatives can be calculated. The best explanation is most often identified with the most probable (see Bayesian decision theory). Acentral rule of Bayesian inference is Bayes' theorem, which gave its name to the field.See Bayesian inference for examples.[edit] Nonmonotonic logic[1]A relation of inference is monotonic if the addition of premises does not undermine previously reached conclusions; otherwise the relation is nonmonotonic. Deductive inference, is monotonic: if a conclusion is reached on the basis of a certain set of premises, then that conclusion still holds if more premises are added.By contrast, everyday reasoning is mostly nonmonotonic because it involves risk: we jump to conclusions from deductively insufficient premises. We know when it is worth or even necessary (e.g. in medical diagnosis) to take the risk. Yet we are also aware that such inference is defeasible—that new information may undermine old conclusions. Various kinds of defeasible but remarkably successful inference have traditionally captured the attention of philosophers (theories of induction, Peirce’s theory of abduction, inference to the best explanation, etc.). More recently logicians have begun to approach the phenomenon from a formal point of view. The result is a large body of theories at the interface of philosophy, logic and artificial intelligence.[edit] See alsoReasoningo Abductive reasoningo Deductive reasoningo Inductive reasoningo Retroductive reasoning ?EntailmentAnalogyAxiomBayesian inferenceBusiness ruleBusiness rules engine Fuzzy logic Immediate inferenceInference engineInquiryLogicLogic of informationLogical assertionLogical graphNonmonotonic logicRule of inferenceList of rules of inference Theorem Expert systemSherlock Holmes。

SCADE
Page 5
02.02.09
SCADE in Rail Transportation Applications
Interlocking systems control Signaling Ground stations Automatic Train Operations Train Control Systems Critical Graphics Displays Level Crossings Safe Platforms
SCADE
Page 12
02.02.09
SCADE Workspace
1
Workspace Output Shortcuts Editing views
2
3
4
SCADE
Page 13
02.02.09
Lustre
Synchronous dataflow programming language
- Operating on streams – Sequence of values for a variable - Synchronous: discrete time =
Cycle detection
- Inconsistent State Machines may end up in algebraic loops
SCADE
Page 17
02.02.09
Model Simulation
Run interactive simulation sessions to –
Semantic checking
- Determines whether the model conforms to SCADE language semantics

t distribution 学生t分布t number t数t statistic t统计量t test t检验t1topological space t1拓扑空间t2topological space t2拓扑空间t3topological space 分离空间t4topological space 正则拓扑空间t5 topological space 正规空间t6topological space 遗传正规空间table 表table of random numbers 随机数表table of sines 正弦表table of square roots 平方根表table of values 值表tabular 表的tabular value 表值tabulate 制表tabulation 造表tabulator 制表机tacnode 互切点tag 标签tame 驯顺嵌入tame distribution 缓增广义函数tamely imbedded 驯顺嵌入tangency 接触tangent 正切tangent bundle 切丛tangent cone 切线锥面tangent curve 正切曲线tangent function 正切tangent line 切线tangent of an angle 角的正切tangent plane 切平面tangent plane method 切面法tangent surface 切曲面tangent vector 切向量tangent vector field 切向量场tangent vector space 切向量空间tangential approximation 切线逼近tangential component 切线分量tangential curve 正切曲线tangential equation 切线方程tangential stress 切向应力tangents method 切线法tape 纸带tape inscription 纸带记录tariff 税tautology 重言taylor circle 泰勒圆taylor expansion 泰勒展开taylor formula 泰勒公式taylor series 泰勒级数technics 技术technique 技术telegraph equation 电报方程teleparallelism 绝对平行性temperature 温度tempered distribution 缓增广义函数tend 倾向tendency 瞧tension 张力tensor 张量tensor algebra 张量代数tensor analysis 张量分析tensor bundle 张量丛tensor calculus 张量演算法tensor density 张量密度tensor differential equation 张量微分方程tensor field 张量场tensor form 张量形式tensor form of the first kind 第一张量形式tensor function 张量函数tensor of torsion 挠率张量tensor product 张量乘积tensor product functor 张量乘积函子tensor representation 张量表示tensor space 张量空间tensor subspace 张量子空间tensor surface 张量曲面tensorial multiplication 张量乘法term 项term of higher degree 高次项term of higher order 高次项term of series 级数的项terminability 有限性terminable 有限的terminal decision 最后判决terminal edge 终结边terminal point 终点terminal unit 级端设备terminal vertex 悬挂点terminate 终止terminating chain 可终止的链terminating continued fraction 有尽连分数terminating decimal 有尽小数termination 终止terminology 专门名词termwise 逐项的termwise addition 逐项加法termwise differentiation 逐项微分termwise integration 逐项积分ternary 三元的ternary connective 三元联结ternary form 三元形式ternary notation 三进制记数法ternary number system 三进制数系ternary operation 三项运算ternary relation 三项关系ternary representation og numbers 三进制记数法tertiary obstruction 第三障碍tesseral harmonic 田形函数tesseral legendre function 田形函数test 检验test for additivity 加性检验test for uniform convergence 一致收敛检验test function 测试函数test of dispersion 色散检验test of goodness of fit 拟合优度检验test of hypothesis 假设检验test of independence 独立性检验test of linearity 线性检验test of normality 正规性检验test point 测试点test routine 检验程序test statistic 检验统计量tetracyclic coordinates 四圆坐标tetrad 四元组tetragon 四角形tetragonal 正方的tetrahedral 四面角tetrahedral angle 四面角tetrahedral co ordinates 四面坐标tetrahedral group 四面体群tetrahedral surface 四面曲面tetrahedroid 四面体tetrahedron 四面形tetrahedron equation 四面体方程theorem 定理theorem for damping 阻尼定理theorem of alternative 择一定理theorem of identity for power series 幂级数的一致定理theorem of implicit functions 隐函数定理theorem of mean value 平均值定理theorem of principal axes 轴定理theorem of residues 残数定理theorem of riemann roch type 黎曼洛赫型定理theorem on embedding 嵌入定理theorems for limits 极限定理theoretical curve 理论曲线theoretical model 理论模型theory of automata 自动机理论theory of cardinals 基数论theory of complex multiplication 复数乘法论theory of complexity of computations 计算的复杂性理论theory of correlation 相关论theory of differential equations 微分方程论theory of dimensions 维数论theory of elementary divisors 初等因子理论theory of elementary particles 基本粒子论theory of equations 方程论theory of errors 误差论theory of estimation 估计论theory of functions 函数论theory of games 对策论theory of hyperbolic functions 双曲函数论theory of judgment 判断论theory of numbers 数论theory of ordinals 序数论theory of perturbations 摄动理论theory of probability 概率论theory of proportions 比例论theory of relativity 相对论theory of reliability 可靠性理论theory of representations 表示论theory of sets 集论theory of sheaves 层理论theory of singularities 奇点理论theory of testing 检验论theory of time series 时间序列论theory of transversals 横断线论theory of types 类型论thermal 热的thermodynamic 热力学的thermodynamics 热力学theta function 函数theta series 级数thick 厚的thickness 厚度thin 薄的thin set 薄集third boundary condition 第三边界条件third boundary value problem 第三边界值问题third fundamental form 第三基本形式third isomorphism theorem 第三同构定理third proportional 比例第三项third root 立方根thom class 汤姆类thom complex 汤姆复形three body problem 三体问题three dimensional 三维的three dimensional space 三维空间three dimensional torus 三维环面three eighths rule 八分之三法three faced 三面的three figur 三位的three place 三位的three point problem 三点问题three series theorem 三级数定理three sheeted 三叶的three sided 三面的three sigma rule 三规则three termed 三项的three valued 三值的three valued logic 三值逻辑three valued logic calculus 三值逻辑学threshold logic 阈逻辑time interval 时程time lag 时滞time series analysis 时序分析timesharing 分时toeplitz matrix 托普利兹矩阵tolerance 容许tolerance distribution 容许分布tolerance estimation 容许估计tolerance factor 容许因子tolerance level 耐受水平tolerance limit 容许界限tolerance region 容许区域top digit 最高位数字topological 拓扑的topological abelian group 拓扑阿贝耳群topological algebra 拓扑代数topological cell 拓扑胞腔topological circle 拓扑圆topological completeness 拓扑完备性topological complex 拓扑复形topological convergence 拓扑收敛topological dimension 拓扑维topological direct sum 拓扑直和topological dynamics 拓扑动力学topological embedding 拓扑嵌入topological field 拓扑域topological group 拓扑群topological homeomorphism 拓扑同胚topological index 拓扑指数topological invariant 拓扑不变量topological limit 拓扑极限topological linear space 拓扑线性空间topological manifold 拓扑廖topological mapping 拓扑同胚topological pair 拓扑偶topological polyhedron 曲多面体topological product 拓扑积topological residue class ring 拓扑剩余类环topological ring 拓扑环topological simplex 拓扑单形topological skew field 拓扑非交换域topological space 拓扑空间topological sphere 拓扑球面topological structure 拓扑结构topological sum 拓扑和topological type 拓扑型topologically complete set 拓扑完备集topologically complete space 拓扑完备空间topologically equivalent space 拓扑等价空间topologically nilpotent element 拓扑幂零元topologically ringed space 拓扑环式空间topologically solvable group 拓扑可解群topologico differential invariant 拓扑微分不变式topologize 拓扑化topology 拓扑topology of bounded convergence 有界收敛拓扑topology of compact convergence 紧收敛拓扑topology of uniform convergence 一致收敛拓扑toroid 超环面toroidal coordinates 圆环坐标toroidal function 圆环函数torque 转矩torsion 挠率torsion coefficient 挠系数torsion form 挠率形式torsion free group 非挠群torsion group 挠群torsion module 挠模torsion of a curve 曲线的挠率torsion product 挠积torsion subgroup 挠子群torsion tensor 挠率张量torsion vector 挠向量torsionfree connection 非挠联络torsionfree module 无挠模torsionfree ring 无挠环torus 环面torus function 圆环函数torus group 环面群torusknot 环面纽结total 总和total correlation 全相关total curvature 全曲率total degree 全次数total differential 全微分total differential equation 全微分方程total error 全误差total graph 全图total image 全象total inspection 全检查total instability 全不稳定性total inverse image 全逆象total matrix algebra 全阵环total matrix ring 全阵环total order 全序total predicate 全谓词total probability 总概率total probability formula 总概率公式total regression 总回归total relation 通用关系total space 全空间total stability 全稳定性total step iteration 整步迭代法total step method 整步迭代法total stiefel whitney class 全斯蒂费尔惠特尼类total subset 全子集total sum 总和total variation 全变差totally bounded set 准紧集totally bounded space 准紧空间totally differentiable 完全可微分的totally differentiable function 完全可微函数totally disconnected 完全不连通的totally disconnected graph 完全不连通图totally disconnected groupoid 完全不连通广群totally disconnected set 完全不连通集totally disconnected space 完全不连通空间totally geodesic 全测地的totally nonnegative matrix 全非负矩阵totally ordered group 全有序群totally ordered set 线性有序集totally positive 全正的totally positive matrix 全正矩阵totally quasi ordered set 完全拟有序集totally real field 全实域totally reflexive relation 完全自反关系totally regular matrix method 完全正则矩阵法totally singular subspace 全奇异子空间totally symmetric loop 完全对称圈totally symmetric quasigroup 完全对称拟群touch 相切tournament 竞赛图trace 迹trace form 迹型trace function 迹函数trace of dyadic 并向量的迹trace of matrix 矩阵的迹trace of tensor 张量的迹tracing point 追迹点track 轨迹tractrix 曳物线trajectory 轨道transcendence 超越性transcendence basis 超越基transcendence degree 超越次数transcendency 超越性transcendental element 超越元素transcendental equation 超越方程transcendental function 超越函数transcendental integral function 超越整函数transcendental number 超越数transcendental singularity 超越奇点transcendental surface 超越曲面transfer 转移transfer function 转移函数transfinite 超限的transfinite diameter 超限直径transfinite induction 超限归纳法transfinite number 超限序数transfinite ordinal 超限序数transform 变换transformation 变换transformation equation 变换方程transformation factor 变换因子transformation formulas of the coordinates 坐标的变换公式transformation function 变换函数transformation group 变换群transformation of air mass 气团变性transformation of coordinates 坐标的变换transformation of parameter 参数变换transformation of state 状态变换transformation of the variable 变量的更换transformation rules 变换规则transformation theory 变换论transformation to principal axes 轴变换transgression 超渡transient response 瞬态响应transient stability 瞬态稳定性transient state 瞬态transient time 过渡时间transition function 转移函数transition graph 转换图transition matrix 转移矩阵transition probability 转移函数transitive closure 传递闭包transitive graph 传递图transitive group of motions 可迁运动群transitive law 可迁律transitive permutation group 可迁置换群transitive relation 传递关系transitive set 可递集transitivity 可递性transitivity laws 可迁律translatable design 可旋转试验设计translate 转移translation 平移translation curve 平移曲线translation group 平移群translation invariant 平移不变的translation invariant metric 平移不变度量translation number 殆周期translation of axes 坐标轴的平移translation operator 平移算子translation surface 平移曲面translation symmetry 平移对称translation theorem 平移定理transmission channel 传输通道transmission ratio 传输比transport problem 运输问题transportation algorithm 运输算法transportation matrix 运输矩阵transportation network 运输网络transportation problem 运输问题transpose 转置transposed inverse matrix 转置逆矩阵transposed kernel 转置核transposed map 转置映射transposed matrix 转置阵transposition 对换transversal 横截矩阵胚transversal curve 横截曲线transversal field 模截场transversal lines 截线transversality 横截性transversality condition 横截条件transverse axis 横截轴transverse surface 横截曲面trapezium 不规则四边形trapezoid 不规则四边形trapezoid formula 梯形公式trapezoid method 梯形公式traveling salesman problem 转播塞尔斯曼问题tree 树trefoil 三叶形trefoil knot 三叶形纽结trend 瞧trend line 瞧直线triad 三元组trial 试验triangle 三角形triangle axiom 三角形公理triangle condition 三角形公理triangle inequality 三角形公理triangulable 可三角剖分的triangular decomposition 三角分解triangular form 三角型triangular matrix 三角形矩阵triangular number 三角数triangular prism 三棱柱triangular pyramid 四面形triangular surface 三角曲面triangulate 分成三角形triangulation 三角剖分triaxial 三轴的triaxial ellipsoid 三维椭面trichotomy 三分法trident of newton 牛顿三叉线tridiagonal matrix 三对角线矩阵tridimensional 三维的trigammafunction 三函数trigonometric 三角的trigonometric approximation polynomial 三角近似多项式trigonometric equation 三角方程trigonometric function 三角函数trigonometric moment problem 三角矩问题trigonometric polynomial 三角多项式trigonometric series 三角级数trigonometrical interpolation 三角内插法trigonometry 三角学trihedral 三面形的trihedral angle 三面角trihedron 三面体trilateral 三边的trilinear 三线的trilinear coordinates 三线坐标trilinear form 三线性形式trinomial 三项式;三项式的trinomial equation 三项方程triplanar point 三切面重点 ?triple 三元组triple curve 三重曲线triple integral 三重积分triple point 三重点triple product 纯量三重积triple product of vectors 向量三重积triple root 三重根triple series 三重级数triple tangent 三重切线triply orthogonal system 三重正交系triply tangent 三重切线的trirectangular spherical triangle 三直角球面三角形trisecant 三度割线trisect 把...三等分trisection 三等分trisection of an angle 角的三等分trisectrix 三等分角线trivalent map 三价地图trivector 三向量trivial 平凡的trivial character 单位特贞trivial cohomology functor 平凡上同弹子trivial extension 平凡扩张trivial fibre bundle 平凡纤维丛trivial graph 平凡图trivial homogeneous ideal 平凡齐次理想trivial knot 平凡纽结trivial solution 平凡解trivial subset 平凡子集trivial topology 密着拓扑trivial valuation 平凡赋值triviality 平凡性trivialization 平凡化trochoid 摆线trochoidal 余摆线的trochoidal curve 摆线true error 真误差true formula 真公式true proposition 真命题true sign 直符号true value 真值truncated cone 截锥truncated cylinder 截柱truncated distribution 截尾分布truncated pyramid 截棱锥truncated sample 截样本truncated sequence 截序列truncation 舍位truncation error 舍位误差truncation point 舍位点truth 真值truth function 真值函项truth matrix 真值表truth set 真值集合truth symbol 真符号truth table 真值表truthvalue 真值tube 管tubular knot 管状纽结tubular neighborhood 管状邻域tubular surface 管状曲面turbulence 湍流turbulent 湍聊turing computability 图灵机可计算性turing computable 图灵机可计算的turing machine 图录机turn 转向turning point 转向点twice 再次twice differentiable function 二次可微函数twin primes 素数对twisted curve 空间曲线twisted torus 挠环面two address 二地址的two address code 二地址代码two address instruction 二地址指令two body problem 二体问题two decision problem 二判定问题two digit 二位的two dimensional 二维的two dimensional laplace transformation 二重拉普拉斯变换two dimensional normal distribution 二元正态分布two dimensional quadric 二维二次曲面two dimensional vector space 二维向量空间two fold transitive group 双重可迁群two person game 两人对策two person zero sum game 二人零和对策two phase sampling 二相抽样法two place 二位的two point distribution 二点分布two point form 两点式two sample method 二样本法two sample problem 二样本问题two sample test 双样本检验two sheet 双叶的two sided condition 双边条件two sided decomposition 双边分解two sided divisor 双边因子two sided ideal 双边理想two sided inverse 双边逆元two sided module 双边模two sided neighborhood 双侧邻域two sided surface 双侧曲面two sided test 双侧检定two stage sampling 两阶段抽样法two termed expression 二项式two valued logic 二值逻辑two valued measure 二值测度two variable matrix 双变量矩阵two way array 二向分类two way classification 二向分类twopoint boundary value problem 两点边值问题type 型type problem 类型问题typenumber 型数typical mean 典型平均。

Z3:An Efficient SMT SolverLeonardo de Moura and Nikolaj BjørnerMicrosoft Research,One Microsoft Way,Redmond,WA,98074,USA{leonardo,nbjorner}@Abstract.Satisfiability Modulo Theories(SMT)problem is a decisionproblem for logicalfirst order formulas with respect to combinations ofbackground theories such as:arithmetic,bit-vectors,arrays,and unin-terpreted functions.Z3is a new and efficient SMT Solver freely availablefrom Microsoft Research.It is used in various software verification andanalysis applications.1IntroductionSatisfiability modulo theories(SMT)generalizes boolean satisfiability(SAT)by adding equality reasoning,arithmetic,fixed-size bit-vectors,arrays,quantifiers, and other usefulfirst-order theories.An SMT solver is a tool for deciding the satisfiability(or dually the validity)of formulas in these theories.SMT solvers enable applications such as extended static checking,predicate abstraction,test case generation,and bounded model checking over infinite domains,to mention a few.Z3is a new SMT solver from Microsoft Research.It is targeted at solving problems that arise in software verification and software analysis.Consequently, it integrates support for a variety of theories.A prototype of Z3participated in SMT-COMP’07,where it won4first places,and7second places.Z3uses novel algorithms for quantifier instantiation[4]and theory combination[5].The first external release of Z3was in September2007.More information,including instructions for downloading and installing the tool,is available at the Z3web page:/projects/z3.Currently,Z3is used in Spec#/Boogie[2,7],Pex[13],HAVOC[11],Vigi-lante[3],a verifying C compiler(VCC),and Yogi[10].It is being integrated with other projects,including SLAM/SDV[1].2ClientsBefore describing the inner workings of Z3,two selected uses are briefly de-scribed.Front-ends interact with Z3by using either a textual format or a binary API.Three textual input-formats are supported:The SMT-LIB[12]format,the Simplify[8]format,and a low-level native format in the spirit of the DIMACS format for propositional SAT formulas.One can also call Z3procedurally by using either an ANSI C API,an API for managed common language runtime,or an OCaml API.Spec#/Boogie generates logical verification conditions from a Spec#pro-gram(an extension of C#).Internally,it uses Z3to analyze the verification conditions,to prove the correctness of programs,or tofind errors on them.The formulas produced by Spec#/Boogie contain universal quantifiers,and also use linear integer arithmetic.Spec#replaced the Simplify theorem prover by Z3as the default reasoning engine in May2007,resulting in substantial performance improvements during theorem proving.Pex(Program EXploration)is an intelligent assistant to the programmer.By automatically generating unit tests,it allows tofind bugs early.In addition,it suggests to the programmer how tofix the bugs.Pex learns the program behavior from the execution traces,and Z3is used to produce new test cases with different behavior.The result is a minimal test suite with maximal code coverage.The formulas produced by Pex containsfixed-sized bit-vectors,tuples,arrays,and quantifiers.3System ArchitectureZ3integrates a modern DPLL-based SAT solver,a core theory solver that han-dles equalities and uninterpreted functions,satellite solvers(for arithmetic,ar-rays,etc.),and an E-matching abstract machine(for quantifiers).Z3is imple-mented in C++.A schematic overview of Z3is shown in the followingfigure.Simplifier Input formulas arefirst processed using an incomplete,but efficient simplification.The simplifier applies standard algebraic reduction rules,such as p∧true→p,but also performs limited contextual simplification,as it identifies equational definitions within a context and reduces the remaining formula using the definition,so for instance x=4∧q(x)→x=4∧q(4).The trivially satisfiable conjunct x=4is not compiled into the core,but kept aside in the case the client requires a model to evaluate x.Compiler The simplified abstract syntax tree representation of the formula is converted into a different data-structure comprising of a set of clauses and congruence-closure nodes.Congruence Closure Core The congruence closure core receives truth assign-ments to atoms from the SAT solver.Atoms range over equalities and theory specific atomic formulas,such as arithmetical inequalities.Equalities asserted by the SAT solver are propagated by the congruence closure core using a data structure that we will call an E-graph following[8].Nodes in the E-graph may point to one or more theory solvers.When two nodes are merged,the set of theory solver references are merged,and the merge is propagated as an equality to the theory solvers in the intersection of the two sets of solver references.The core also propagates the effects of the theory solvers,such as inferred equalities that are produced and atoms assigned to true or false.The theory solvers may also produce fresh atoms in the case of non-convex theories.These atoms are subsequently owned and assigned by the SAT solver.Theory Combination:Traditional methods for combining theory solvers rely on capabilities of the solvers to produce all implied equalities or a pre-processing step that introduces additional literals into the search space.Z3uses a new theory combination method that incrementally reconciles models maintained by each theory[5].SAT Solver Boolean case splits are controlled using a state-of-the art SAT solver.The SAT solver integrates standard search pruning methods,such as two-watch literals for efficient Boolean constraint propagation,lemma learning using conflict clauses,phase caching for guiding case splits,and performs non-chronological backtracking.Deleting clauses:Quantifier instantiation has a side-effect of producing new clauses containing new atoms into the search space.Z3garbage collects clauses, together with their atoms and terms,that were useless in closing branches.Con-flict clauses,and literals used in them,are on the other hand not deleted,so quantifier instantiations that were useful in producing conflicts are retained as a side-effect.Relevancy propagation:DPLL(T)based solvers assign a Boolean value to potentially all atoms appearing in a goal.In practice,several of these atoms are don’t cares.Z3ignores these atoms for expensive theories,such as bit-vectors, and inference rules,such as quantifier instantiation.The algorithm used for discriminating relevant atoms from don’t cares is described in[6].Quantifier instantiation using E-matching Z3uses a well known approach for quantifier reasoning that works over an E-graph to instantiate quantified vari-ables.Z3uses new algorithms that identify matches on E-graphs incrementally and efficiently.Experimental results show substantial performance improvements over existing state-of-the-art SMT solvers[4].Theory Solvers Z3uses a linear arithmetic solver based on the algorithm used in Yices[9].The array theory uses lazy instantiation of array axioms.The fixed-sized bit-vectors theory applies bit-blasting to all bit-vector operations,but equality.Model generation Z3has the ability to produce models as part of the output. Models assign values to the constants in the input and generate partial function graphs for predicates and function symbols.4ConclusionZ3is being used in several projects at Microsoft since February2007.Its main applications are extended static checking,test case generation,and predicate abstraction.References1.T.Ball and S.K.Rajamani.The SLAM project:debugging system software viastatic analysis.SIGPLAN Not.,37(1):1–3,2002.2.M.Barnett,K.R.M.Leino,and W.Schulte.The Spec#programming system:An overview.In CASSIS2004,LNCS3362,pages49–69.Springer,2005.3.M.Costa,J.Crowcroft,M.Castro,A.I.T.Rowstron,L.Zhou,L.Zhang,andP.Barham.Vigilante:end-to-end containment of internet worms.In A.Herbert and K.P.Birman,editors,SOSP,pages133–147.ACM,2005.4.L.de Moura and N.Bjørner.Efficient E-matching for SMT Solvers.In CADE’07.Springer-Verlag,2007.5.L.de Moura and N.Bjørner.Model-based Theory Combination.In SMT’07,2007.6.L.de Moura and N.Bjørner.Relevancy Propagation.Technical Report MSR-TR-2007-140,Microsoft Research,2007.7.R.DeLine and K.R.M.Leino.BoogiePL:A typed procedural language for check-ing object-oriented programs.Technical Report2005-70,Microsoft Research,2005.8. D.Detlefs,G.Nelson,and J.B.Saxe.Simplify:a theorem prover for programchecking.J.ACM,52(3):365–473,2005.9. B.Dutertre and L.de Moura.A Fast Linear-Arithmetic Solver for DPLL(T).InCAV’06,LNCS4144,pages81–94.Springer-Verlag,2006.10. B.S.Gulavani,T.A.Henzinger,Y.Kannan,A.V.Nori,and S.K.Rajamani.Syn-ergy:a new algorithm for property checking.In Michal Young and Premkumar T.Devanbu,editors,SIGSOFT FSE,pages117–127.ACM,2006.hiri and S.Qadeer.Back to the Future:Revisiting Precise Program Veri-fication using SMT Solvers.In POPL’2008,2008.12.S.Ranise and C.Tinelli.The Satisfiability Modulo Theories Library(SMT-LIB).,2006.13.N.Tillmann and W.Schulte.Unit Tests Reloaded:Parameterized Unit Testingwith Symbolic Execution.IEEE software,23:38–47,2006.。

句子分析
4.
Or we can say that function f is differentiable only if f is differentiable at a for every a in the domain of f. 或者可以说函数f是可微的，仅当f对 于定义域内所有自变量a都是可微的。

核心单词和词组

Subinterval: 子区间

subregion：分区 subaggregate ：子集 Partition：分割，分区
Subdivide：再分，细分 Elongated：伸长的，变长了的 inf: infimum，下确界 sup: supremum，上确界
核心单词和词组

Tangent:
切线的，相切的，离题的
a tangent line：切线 tangent plane：切面 tangent remarks：扯得离题太远
核心单词和词组
切线，正切
arc tangent：反正切 common tangent：公切线 hyperbolic tangent：双曲线切线; 双曲 正切
Cotangent：余切
核心单词和词组
Secant：切的，割的，交叉的；割线，正
割
arc
secant：反正割 Secant line: 割线 Cosecant：余割 Sine：正弦 Cosine：余弦
核心单词和词组
Concept: 概念 derivational concept：派生概念 potential concept：势差概念 Idea：想法，思想，概念，含义
核心单词和词组Leabharlann Integral 积分