Constructive Negation and Constraints

Mechanized Metatheory Model-CheckingJames Cheney LFCS,University of Edinburgh j cheney@Alberto MomiglianoLFCS,University of Edinburgh/DSI,University ofMilana momigl1@AbstractThe problem of mechanically formalizing and proving metathe-oretic properties of programming language calculi,type systems, operational semantics,and related formal systems has received considerable attention recently.However,the dual problem of searching for errors in such formalizations has received compar-atively little attention.In this paper,we consider the problem of bounded model-checking for metatheoretic properties of formal systems specified using nominal logic.In contrast to the current state of the art for metatheory verification,our approach is fully au-tomatic,does not require expertise in theorem proving on the part of the user,and produces counterexamples in the case that aflaw is detected.We present two implementations of this technique,one based on negation-as-failure and one based on negation elimina-tion,along with experimental results showing that these techniques are fast enough to be used interactively to debug systems as they are developed.Categories and Subject Descriptors D.3.2[Programming Lan-guages]:Language Classifications—Constraint and logic lan-guages; D.2.4[Software Engineering]:Program Verification—Model checking;Assertion checkers; D.2.5[Software Engineer-ing]:Testing and Debugging—Testing tools; F.3.1[Logics and Meaning of Programs]:Specifying and Verifying and Reasoning about Programs—Mechanical verification; F.4.1[Mathematical Logic and Formal Languages]:Mathematical Logic—Logic and constraint programmingGeneral Terms Experimentation,VerificationKeywords nominal logic,model checking,counterexample search1.IntroductionMuch of modern programming languages research is founded on proving properties of interest by syntactic methods,such as cut elimination,strong normalization,or type soundness theo-rems[39].Convincing syntactic proofs are challenging to perform on paper for several reasons,including the presence of variable binding,substitution,and associated equational theories(such as α-equivalence in theλ-calculus and structural congruences in pro-cess calculi),the need to perform reasoning by simultaneous or well-founded induction on multiple terms or derivations,and the Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on thefirst page.To copy otherwise,to republish,to post on servers or to redistribute to lists,requires prior specific permission and/or a fee.PPDP’07July14–16,2007,Wroclaw,Poland.Copyright c 2007ACM978-1-59593-769-8/07/0007...$5.00often large number of cases that must be considered.Paper proofs are believed to be unreliable due in part to the fact that they usu-ally sketch only the essential part of the argument,while leaving out verification of the many subsidiary lemmas and side-conditions needed to ensure that all of the proof steps are correct and that enough cases have been considered.A great deal of attention,recently reinvigorated by the POPLMark Challenge[2],has been focused on the problem of metatheory mechanization,that is,formally verifying such properties using computational tools.Formal,machine-checkable proof is widely agreed to provide the highest possible standard of evidence for believing such a system is correct.However,all extant theorem proving systems that have been employed in metatheory verifi-cation1have high learning curves,and using them to verify the properties of a nontrivial system requires a great deal of effort even after the learning curve has been surmounted,because inductive theorem-proving is currently a brain-bound,not CPU-bound,pro-cess.Moreover,verification attempts provide little assistance in the case of an incorrect system,even though this is the common case during the development of such a system.Verification attempts can fail due to eitherflaws in the system or mistakes on the user’s part. Determining which is the case(and how best to proceed)is part of the arduous process of becoming a power user of a theorem-proving system.These observations about formal verification are not new.They have long been used to motivate model-checking[15].In model-checking,the user specifies the system and describes properties which it should satisfy;it is the computer’s job to search for coun-terexamples or to determine that none exist.Although it was prac-tical only for smallfinite-state systems whenfirst proposed more than25years ago,improved techniques for searching the state space efficiently(such as symbolic model checking using Boolean decision diagrams[28])have now made it feasible to verify in-dustrial hardware designs.As a result,model checking has gained widespread acceptance in industry.We argue that mechanically verified proof is neither the only, nor always the most appropriate,way of gaining confidence in the correctness of a formal system;moreover,it is almost never the most appropriate way to debug such a system.This is certainly the case in the area of hardware verification,where model-checking has surpassed theorem-proving in industrial acceptance and applicabil-ity.Forfinite systems such as hardware designs,model checking is,in principle,able to either guarantee that the design is correct, or produce a concrete counterexample.Model-checking tools are CPU-bound;thus,they can often leverage hardware advances more readily than theorem provers.Model-checkers do not generally re-quire as much expertise as theorem provers;once the model speci-fication and formula languages have been learned,an engineer can formalize a design,specify desired properties,and let the system 1principally theorem provers such as Twelf,Coq,Isabelle/HOL,HOLdo the work.Researchers can(and have)focused on the orthogo-nal issue of representing and exploring the state space efficiently so that the answer is produced as quickly as possible.This separation of concerns has facilitated great progress.We advocate mechanized metatheory model-checking as a use-ful complement to established techniques for analyzing program-ming languages and related systems.Of course,such systems are usually infinite-state,so cannot be automatically verified infinite time,but we can at least automate the search for counterexam-ples over bounded,but arbitrarily large,subsets of the search space. Such bounded model checking(failure tofind a simple counterex-ample)provides a degree of confidence that a design is correct,al-beit not as much confidence as full verification.Nevertheless,this approach shares other advantages of model-checking:it is CPU-bound,not brain-bound;it separates high-level specification con-cerns from low-level implementation issues;and it provides explicit counterexamples.Thus,bounded model checking is likely to be more helpful than verification typically is during the development of a system.In this paper we describe an approach to checking desired prop-erties of formal systems implemented inαProlog,a logic pro-gramming language which supports programming with“concrete”names and binding moduloα-equivalence[11].Our work is the first to show how tofind bugs in high-level specifications of pro-gramming languages and other calculi automatically and effec-tively.We explore techniques based on both negation-as-failure and negation elimination,along with encouraging,though prelim-inary,experimental results.Our experience has been that while brute-force testing cannot yetfind“deep”problems(such as the well-known unsoundness in old versions of ML involving polymor-phism and references)by itself,it is extremely useful for eliminat-ing“shallow”bugs or typos.The structure of the remainder of the paper is as follows.Fol-lowing a brief introduction toαProlog,Section2presents our ap-proach at an informal,tutorial level.Section3introduces the syntax and semantics of a core language forαProlog which we shall use in the rest of the paper.Section4discusses a simple implementa-tion of metatheory model-checking inαProlog based on negation-as-failure(NF).Section5discusses a more sophisticated imple-mentation based on negation elimination(NE),including a discus-sion of the modifications needed to adapt existing negation elimi-nation algorithms toαProlog and a sketch of the soundness proof for the technique.Section6presents experimental results that show that the negation elimination approach may offers performance im-provements over the other approaches we considered.Sections7–9 discuss related and future work and conclude.2.Tutorial Example2.1αProlog BackgroundWe will specify the formal systems whose properties we wish to check,as well as the properties themselves,as Horn clause logic programs inαProlog.αProlog is a logic programming language based on nominal logic,afirst-order theory axiomatizing names and name-binding introduced by Pitts[40]and based on Gabbay and Pitts’swapping-based approach to binding syntax[20].Unlike ordinary Prolog,αProlog is typed;all constants,function symbols, and predicate symbols must be declared explicitly.We provide a brief review in this section and a more detailed discussion of a monomorphic core language forαProlog in Section3;many more details,including a detailed semantics,can be found in[11,12].InαProlog,there are several built-in types,functions and re-lations with special behavior.There are distinguished name types which are are populated with infinitely many name constants.In program text,a name constant is generally a lower-case symbol id:name_type.tm:type.ty:type.var:id->tm.unit:tm.app:(tm,tm)->m:id\tm->tm.pair:(tm,tm)->tm.fst:tm->tm.snd:tm->tm.func sub(tm,id,tm)=tm.sub(var(X),X,N)=N.sub(var(X),Y,N)=var(Y):-X#Y.sub(app(M1,M2),Y,N)=app(sub(M1,Y,N),sub(M2,Y,N)). sub(lam(x\M),Y,N)=lam(x\sub(M,Y,N)):-x#(Y,N). sub(unit,Y,N)=unit.sub(pair(M1,M2),Y,N)=pair(sub(M1,Y,N),sub(M1,Y,N)). sub(fst(M),Y,N)=fst(sub(M,Y,M)).sub(fst(M),Y,N)=snd(sub(M,Y,N)).#check"sub_fun"5:sub(M,x,N)=M1,sub(M,x,N)=M2=>M1=M2.#check"sub_id"5:sub(M,x,var(x))=M.#check"sub_fresh"5:x#M=>sub(M,x,N)=M.#check"sub_sub"5:x#N’=>sub(sub(M,x,N),y,N’)=sub(sub(M,y,N’),x,sub(N,y,N’)).Figure1.Terms and substitutionthat has not been declared as something else(such as a predicate or function symbol).Names can be used in abstractions,written a\M in programs.Abstractions are considered equal up toα-renaming of the bound name for the purposes of unification inαProlog.Thus, where one writesλx.M,νx.M,etc.in a paper exposition,inαPro-log one writes lam(x\M),nu(x\M),etc.In addition,the freshness relation a#t holds between a name a and a term t that does not contain a free occurrence of a.Thus,where one would write x∈F V(t)in a paper exposition,inαProlog one writes x#t.Horn clause logic programs over these operations suffice to de-fine a wide variety of core languages,type systems,and operational semantics in a convenient way.Moreover,Horn clauses can also be used as specifications of desired program properties,including ba-sic lemmas concerning substitution as well as main theorems such as preservation,progress,and type soundness.We therefore con-sider the problem of checking specifications#check"spec"n:A1,...,An=>C.where spec is a label naming the property,n is a parameter that bounds the search space,and A1through An and C are atomic for-mulas describing the preconditions and conclusion of the prop-erty.As with program clauses,the specification formula is implic-itly universally quantified.As a simple,running example,we con-sider the lambda-calculus with units,pairs,and function types to-gether with appropriate specifications of properties that one usually wishes to verify.Terms and substitution In contrast to other techniques such as higher-order abstract syntax,there is no built-in substitution oper-ation inαProlog,so we must define it explicitly.However,sub-stitution can be defined declaratively inαProlog;see Figure1. For convenience,αProlog provides a function-definition syntax, but this is presently just translated to an equivalent(but far more verbose)relational implementation,usingflattening(more sophis-ticated functional logic programming techniques,such as narrow-ing[21],would require the development of novel nominal equa-tional unification algorithms).After the definition of the sub function,we have added some directives that state desired properties of substitution that we wishunitTy:ty.==>:ty->ty->ty.infixr==>5.**:ty->ty->ty.infixl**6.type ctx=[(id,ty)].pred wf_ctx(ctx).wf_ctx([]).wf_ctx([(X,T)|G]):-X#G,wf_ctx(G).pred tc(ctx,tm,ty).tc([(V,T)|G],var(V),T).tc(G,lam(x\E),T1==>T2):-tc([(x,T1)|G],E,T2).tc(G,app(E1,E2),T):-tc(G,E1,T==>T0),tc(G,E2,T0).tc(G,pair(M,N),T1**T2):-tc(G,M,T1),tc(G,N,T2).tc(G,fst(M),T1):-tc(G,M,T1**T2).tc(G,snd(M),T1):-tc(G,M,T1**T2).tc(G,unit,unitTy).#check"tc_weak"5:x#G,tc(G,E,T)=>tc([(x,T’)|G],E,T).#check"tc_sub"5:x#G,tc(G,E,T),tc([(x,T)|G],E’,T’),wf_ctx(G)=>tc(G,sub(E’,x,E),T’).Figure2.Types,contexts,and well-formednessto check.First,the sub_fun property states that the result of sub-stitution is uniquely defined.Since sub is internally translated to a relation in the current implementation(and since mode and de-terminism analysis are not yet available inαProlog),this is some-thing we ought to check.Second,sub_id checks that substituting a variable with itself has no effect.The sub_fresh property is the familiar lemma that substituting has no effect if the variable is not present in M;the last property sub_sub is a standard substitution commutation lemma.Types and typechecking Next we turn to types and typechecking, Figure2.We introduce constructors for simple types including unit, pairing,and function types.The typechecking judgment is stan-dard.In addition,we check some standard properties of typecheck-ing,including weakening(tc_weak)and the substitution lemma (tc_sub).Note that since we are merely specifying,not proving, the substitution lemma,we do not have to state its general form. However,since contexts are encoded as lists of pairs of variables and types,we do have to explicitly define what it means for a con-text to be well-formed:contexts must not contain multiple bindings for the same variable.This is specified using the wf_ctx predicate. Evaluation and soundness Now we arrive at the main point of this example,namely defining the operational semantics and checking that the type system is sound with respect to it,Figure3. Wefirst define values,introduce one-step and multi-step call-by-value reduction relations,define the progress relation indicating that a term is not stuck,and specify type preservation(tc_pres), progress(tc_prog),and soundness(tc_sound)properties.2.2Specification checkingThe alert reader may have noticed several errors in the program above.In fact,every specification we have ascribed to it is violated. Some of the bugs were introduced deliberately,others were discov-ered while debugging the specification using an early version of the checking tool.Before proceeding,the reader may wish to try to find all of the errors using his or her preferred formal verification method.We now describe the results of the specification checker on the above program,along the way giving intuition concerning the pred value(tm).value(lam(_)).value(b).value(pair(V,W)):-value(V),value(W).pred step(tm,tm).step(app(lam(x\M),N),sub(N,x,M)).step(app(M,N),app(M’,N)):-step(M,M’).step(pair(M,N),pair(M’,N)):-step(M,M’).step(pair(V,N),pair(V,N’)):-value(V),step(N,N’). step(fst(M),fst(M’)):-step(M,M’).step(fst(pair(V,_)),V):-value(V).step(fst(M),fst(M’)):-step(M,M’).step(snd(pair(_,V)),V):-value(V).pred progress(tm).progress(V):-value(V).progress(M):-step(M,_).pred steps(exp,exp).steps(M,M).steps(M,P):-step(M,N),steps(N,P).#check"tc_pres"5:tc([],M,T),step(M,M’)=>tc([],M’,T).#check"tc_prog"5:tc([],E,T)=>progress(E).#check"tc_sound"5:tc(empty,E,T),steps(E,E’)=>tc(empty,E’,T).Figure3.Reduction,type preservation,progress,and soundness counterexample search strategy.First,consider the substitution specifications.The specification checker produces the following typical(though slightly sanitized)output for thefirst two: Checking for counterexamples tosub_fun:sub(M,x,N)=M1,sub(M,x,N)=M2=>M1=M2 Checking depth123Counterexample found:M=fst(var(x)),M1=fst(var(x)),M2=snd(var(V)),N=var(V)--------Checking for counterexamples tosub_id:sub(M,x,var(x))=MChecking depth12Counterexample found:M=var(V1)x#V1Thefirst error is due to the following bug:sub(fst(M),Y,N)=snd(sub(M,Y,N))should besub(snd(M),Y,N)=snd(sub(M,Y,N))Of course,this kind of problem could also be detected by a mode analysis(which has,however,not yet been developed forαProlog).The second error appears to be due to the typo in the clause sub(var(X),Y,N)=var(Y):-X#Y.which should besub(var(X),Y,N)=var(X):-X#Y.Afterfixing these errors,no more counterexamples are found for”sub fun”,but we haveChecking for counterexamples tosub_id:sub(M,x,var(x))=MChecking depth1234Counterexample found:M=pair(var(x),b)Looking at the relevant clauses,we notice thatsub(pair(M1,M2),Y,N)=pair(sub(M1,Y,N),sub(M1,Y,N)). should besub(pair(M1,M2),Y,N)=pair(sub(M1,Y,N),sub(M2,Y,N)).After thisfix,the only remaining counterexample involving substitution isChecking for counterexamples tosub_id:sub(M,x,var(x))=MChecking depth1234Counterexample found:M=fst(lam(x4877\var(x)))The culprit is this clausesub(fst(M),Y,N)=fst(sub(M,Y,M)).which should besub(fst(M),Y,N)=fst(sub(M,Y,N)).Once these bugs have beenfixed,the tc_sub property checks out,but tc_weak and tc_pres are still violated:Checking for counterexamples totc_weak:x#G,tc(G,E,T),wf_ctx(G)=>tc([(x,T’)|G],E,T) Checking depth1234Counterexample found:E=var(V)G=[(V,base)]T=baseT’=base==>base--------Checking for counterexamples totc_pres:tc([],M,T),step(M,M’)=>tc([],M’,T)Checking depth123456Counterexample found:M=app(lam(x\fst(var(x))),b)M’=bT=base**TFor tc_weak,of course we have to change the too-specific clausetc([(V,T)|G],var V,T).totc(G,var V,T):-mem((V,T),G).For tc_pres,M should never have typechecked at type T,and the culprit is the application rule:tc(G,app(E1,E2),T):-tc(G,E1,T==>T0),tc(G,E2,T0).Here,the types in thefirst subgoal are backwards,and should betc(G,app(E1,E2),T):-tc(G,E1,T0==>T),tc(G,E2,T0).Some bugs remain after these corrections,but they are all de-tected by the checker.In particular,the clausestc(G,snd(M),T1):-tc(G,M,T1**T2).step(app(lam(x\M),N),sub(N,x,M)).should be changed totc(G,snd(M),T2):-tc(G,M,T1**T2).step(app(lam(x\M),N),sub(M,x,N)).After making these corrections,none of the specifications produce counterexamples up to the depth bounds shown.3.Core languageThe implementation ofαProlog includes a number of high-level conveniences including parameterized types such as lists,poly-morphism,function definition notation(as used in subst above), and non-logical features such as negation-as-failure and the“cut”proof-search pruning operator.For the purposes of metatheory model-checking we consider only input programs within a smaller, better-behaved fragment for which the semantics(and accompany-ing implementation techniques)are well-understood[12,11,10, 48].In particular,to simplify the presentation we consider only monomorphic,non-parametric types.A signatureΣ=(ΣD,ΣN,ΣF)consists of setsΣD andΣN of base data typesδand name typesν,respectively,together with a collectionΣF of function symbol declarations f:τ→δ.Here, typesτare formed according to the following grammar:τ::=1|δ|τ×τ |ν| ν τwhereδ∈ΣD andν∈ΣN.We consider constants of typeδto be function symbols of arity1→δ.Given a signature,the language of terms over sets V of variables x,y,z,...and A of names a,b,...is defined by the following grammar:t,u::=a|π·X| | t,u | a tπ::=id|(a b)◦πWe say that a term is ground if it has no variables(but possibly does contain names).Suspended permutations appearing before variables are often omitted,that is,we write X for id·X.The abstract syntax a t is synonymous with the concrete syntax a\t for name-abstraction.The swapping operation is defined as follows on ground terms:π· = π·f(t)=f(π·t)π· t,u = π·t,π·uπ·a=π(a)π· a t= π·a π·twhereπ(a)denotes the result of applying the permutationπ(con-sidered as a function)to a.We consider atomic formulae for equality(t≈u)and freshness (t#u),where t is a term of some name type.The freshness relation is defined on ground terms using the following inference rules:(a·=b)a#b a#a#ta#f(t)a#t a#ua# t,ua#b a#ta# b t a# a tSimilarly,the equality relation,which identifies abstractions up to “safe”renaming,is defined on ground terms as follows:a≈a c≈ct1≈u2t2≈u2t1,t2 ≈ u1,u2t≈uf(t)≈f(u)a≈b t≈ua t≈b ua#(b,u)t≈(a b)·ua t≈b uGiven a signature which includes a distinguished base type o of propositions along with predicate symbols p:τ→o,we consider goal and(definite)program clause formulas G and D,respectively, defined by the following grammar:A::=t≈u|t#uG::=⊥| |A|p(t)|G∧G |G∨G|∃X:τ.G|∀X:τ.G|Na:ν.GD::= |p(t)|G⊃D|D∧D |∀X:τ.DΓ:∇|=C Γ:∆;∇⇒C con Γ:∆;∇⇒G 1Γ:∆;∇⇒G 2Γ:∆;∇⇒G 1∧G 2∧RΓ:∆;∇⇒G iΓ:∆;∇⇒G 1∨G 2∨R iΓ:∇|=∃X :τ.C Γ,X :τ:∆;∇,C ⇒GΓ:∆;∇⇒∃X :τ.G∃RΓ:∇|=∀X :τ.C Γ,X :τ:∆;∇,C ⇒GΓ:∆;∇⇒∀X :τ.G ∀RΓ:∇|=Na :ν.C Γ#a :ν:∆;∇,C ⇒G Γ:∆;∇⇒N a :ν.GNRΓ:∆;∇D−→A D ∈∆Γ:∆;∇⇒Aselt ≈uΓ:∆;∇p (t )−→p (u )hypΓ:∆;∇D i−→A Γ:∆;∇D 1∧D 2−→A∧L iΓ:∆;∇D−→A Γ:∆;∇⇒GΓ:∆;∇G ⊃D−→A⊃LΓ:∇|=∃X :τ.CΓ,X :τ:∆;∇,C D−→AΓ:∆;∇∀X :τ.D−→A∀LFigure 4.Proof search semantics of αProlog programsThe novel features of nominal logic programs consist of the fresh-ness and equality constraints (t #u,t ≈u )described above and the Gabbay-Pitts fresh-name quantifier N .The latter,intuitively,quantifies over names not appearing in the formula (or in the val-ues of its variables);that is,provided the free variables and namesof φare {a , X },the formula Na :ν.φis logically equivalent to ∃A :ν.A # X∧φ.Although we permit programs to be defined using arbitrary (sets of)definite clauses ∆,we take advantage of the fact that such programs can always be normalized to sets of clauses of the form ∀ X.G ⊃p (t ).It is useful to single out in a normalized program ∆all the clauses that belong to the definition of a predicate;thus,we define def (p,∆)={D |D ∈∆,D =∀ X.G ⊃p (t )}.As mentioned earlier,the implementation of αProlog includes a notationally convenient syntax for defining functions.Func-tions f of n arguments can be defined using clauses of the form f ( t )=u :−G ;these are translated to n +1-ary predicate clauses p f ( t ,u ):−G .Uses of f within goals such as G [f ( t )]are trans-lated to subgoals of the form ∃X.p f ( t ,X )∧G [X ].A similar technique can be used to provide more convenient elimination forms for pair and abstraction types.The projection functions πi :τ1×τ2→τi can be defined directly using the equation πi (X 1,X 2)=X i .The elimination form for abstraction,called concretion and written t @a ,can be implemented by trans-lating G [t @a ]to ∃X.t ≈ a X ∧G [X ].We use these elimination forms freely in the rest of the paper,subject to the proviso that they must be expanded before any program transformations are applied.Finally,concrete-syntax program clauses containing free names and variables such astc(G,lam(x\M),T ==>U):-x #G,tc([(x,T)|G],M,U).are viewed as equivalent to closed formulas such as:∀G,F,T,U.(N x .F = x M ∧x #G ∧tc ([(x ,T )|G ],M,U ))⊃tc (G,lam (F ),T =⇒U )Note that this transformation yields a proper definite clause in which Nis used only in the subgoal.Such clauses have been studied in previous work [12,48]and it is known that resolution based on nominal unification is sound and complete for proof search for this case,in contrast to the general case where a more complicated equivariant unification problem must be solved [7].We define contexts Γto be sequences of bindings of names or of variables:Γ::=·|Γ,X :τ|Γ#a :νNote that names in closed formulas are always introduced using the N-quantifier;as such,names in a context are always intended to be fresh with respect to the values of variables and other names already in scope when introduced.For this reason,we write name-bindings as Γ#a :ν.We define constraints to be G -formulas of the following form:C ::=t ≈u |t #u |C ∧C |∃X :τ.C |∀X :τ.C |N a :ν.CWe write ∇for a set of constraints.Constraint-solving is modeled by the satisfiability judgment Γ:∇|=C .For constraints ∇,C containing only free variables/names from Γ,this judgment means that for every ground instantiation θof the variables consistent with freshness assertions in Γ,if θ(∇)holds,then θ(C )holds.Efficient algorithms for constraint solving and unification for nominal terms of the above form and for freshness constraints of the form a #t were studied by Urban,Pitts,and Gabbay [49].Note,however,that we also consider freshness constraints of the form π·X #π ·Y .These constraints are needed to express the alpha-inequality predicate neq (see Section 5.2).Constraint solv-ing and satisfiability become NP-hard in the presence of these con-straints [13,Ch.7].In the current implementation,such constraints are delayed until the end of proof search,and any remaining con-straints of the form π·X #π·X are checked for consistency by brute force;these are essentially finite domain constraints.Any remaining constraints π·X #π ·Y where X and Y are not necessarily equal are always satisfiable.We use here a proof-theoretic model of the semantics of αPro-log programs,introduced in [10,12],and shown here in Figure 4.This semantics allows us to focus on the high-level proof searchissues relevant to proving the correctness of negation elimination,without requiring us to introduce or manage low-level operational details concerning constraint solving.The only novelty is the pres-ence of rules for universally quantified goals,which are handled here as in λProlog.The semantics defines two judgments:goal-directed or uniform proof search Γ:∆;∇⇒G ,and programclause-directed or focused proof search Γ:∆;∇D−→A ,where ∆is a set of clauses and ∇a set of constraints.4.Implementation using negation-as-failureWe consider informal #check specifications to correspond to spec-ification formulas of the formNa .∀ X.H 1∧···∧H n ⊃A (1)where H 1,...,H n ,A are atomic formulas (including equality andfreshness constraints).A (finite)counterexample is a closed sub-stitution θsuch that θ(H 1),...,θ(H n )all hold (that is,are deriv-able),but the conclusion θ(A )finitely fails (that is,is not derivable in finitely many steps).We define the bounded model checking problem for such pro-grams and properties as follows:given a resource bound (e.g .a bound on the sizes of counterexamples or number of inference steps needed),decide whether a counterexample can be derived using the given resources,and if so,compute such a counterexample.We consider two approaches to solving this problem using negation-as-failure.First,in principle,we could simply enumer-ate all possible valuations and test them,using negation-as-failure.。

THE SEVEN PRINCIPLESThe use of a technique is always dependent upon the application of a certain number of principles. This is what we call the instructions. One need not follow the rules recommended in such instructions. Indeed the product, device or system for which they were devised may well work even if they are not observed, but will do so less efficiently. Furthermore, the simpler the instructions, the more likely the user is to follow them. The same applies to note-taking. A few very simple principles give this system its sound base and precision, and make using it straightforward. There are seven of these principles; in order they are:1 Noting the idea and not the word2 The rules of abbreviation3 Links4 Negation5 Adding emphasis6 Verticality7 ShiftSome of these principles have already been explained by Jean Herbert in his Interpreter’s Handbook1.1. Noting the idea rather than the wordTake any French text and give it to 10 excellent english translators. The result will be ten very well translated texts, but ten very different texts in as far as the actual words used are concerned. The fact that we have ten good translations, but ten different texts, shows that what is important is the translation of the idea and not the word. This is even truer of interpretation since the interpreter must produce a version of the text in another language immediately. He must be free of the often misleading constraints that words represent. It is through the analysis and notation of the ideas that the interpreter will avoid mistakes and a laboured delivery.Example: Let us take the following, from French into English: …Il y a des fortes chances pour que...../ There is a very good chance that...” If we base our notation of this expression on the words, the key word is chance. If we base it on the idea, it is probable.The notes will have to be read 20 minutes – even an hour2– after the idea was originally expressed. In the first example it would be very easy to make a mistake. Having noted chance the i nterpreter might, if the context allowed, render it …there is a chance that” or …by chance”. If on the other hand he noted probable the mistake cannot be made. The issue of style is also dealt with in the second example where one would automatically say (interpreting into English), …It is probable that”, or …it is likely that”, or …in all likelihood” whereas in the first example even if the interpreter had correctly recalled the idea that the word chance represented he/she will be a prisoner to that word and might easily produce a gallicism3.1 Georg & C ie, Geneva, 1956.2 this was indeed the case when Rozan wrote. Although nowadays 20 minutes is considered a long consecutive speech, his comments still apply.3 being unduly influenced by the source language is, of course, not only a problem in French-English interpretation but in all interpretation.Example: …We should try to live up to....”. It would be absurd to note the word …live” and it would greatly increase the risk of making a mistake. Although it would seem to be very different from the original it woul d be more appropriate to note in French, for example, … à la hauteur” (in english ‘to be up to’). This is the result of analysing the idea behind what is said and noting it idiomatically in the target language. It would be just as useful to note be =, representing being equal to , which could very easily be read back idiomatically in intepretation (ie. …à la hauteur in French”, …to be up to in English”).Whenever taking notes the interpreter must concentrate on the major idea and how this can be noted clearly and simply (preferably in the target language, although this is not essential).In the practical exercises in Part 3 of this book you will find a number of examples of noting the idea rather than the word. It is recommended that you examine these with particular care.2. The Rules of AbbreviationA. ABBREVIATION OF WORDSThe rule of thumb is that unless a word is short (4-5 letters) the interpreter should note it in an abbreviated form.If we have to note …specialized” it is more meaningful a nd reliable to note sp ed than to write spec.Other examples:Stat.could be read as …statute” or …statistics” whilst St ute and St ics are unambiguous.Prod.could be read as …production”, …producer”, …product” or …productivity” whilePr on, Pr er, Pr ct, Pr vity are unambiguous.Com.could be read as …Commission” or …committee” while C on and C tee are unambiguous.Rule: If you have time write a word as completely as possible, however, if a word must be abbreviated, then write some of the first and last letters rather than trying to write as many letters as possible from the start onwards.B. INDICATING GENDER AND TENSEHaving abbreviated a word or an idea (be it by the use of a symbol or a contraction of its component letters) it can also be very helpful to give an indication of gender4 and tense).Thus in the expression: …I will come back to this a little later”, noting the future tense will render the words …a little later”superfluous. We will see below that …I speak” can be noted : I ”. Therefore we note : I ll”The expression: …those mentioned”, must be noted : rf d; because rf alone could be read back as …those which mention”.4 Rozan was working from and into French. Gender is meaningless for those noting in English, however, the idea could be usefully adapted for use in, for example, the Slavic languages where nouns have gender.Rule: To indicate gender5 and number we add e or s to the symbol or abbreviation. To indicate tense we add ll for the future and d for the past.See also the examples in Part 3.C. ABBREVIATING THE REGISTERThe expression …which have contributed to” is long. The word help is short. Wherever possible we must abbreviate by using a word which conveys the same meaning but is shorter.Similarly, …...which are worth looking at” can be noted int g (interesting).…In order to arrive at some conclusions” can be noted to end.…Taking into account the situation at the present time” can be noted as sit on now.Examine closely the abbreviations in Part 3.3. LinksThe part of any speech that is both the most important and the most difficult to note is the sequence of ideas and the links between them. (Jean Herbert)An idea can be distorted completely if its relation to the previous idea is not clearly indicated. When taking notes then, we should never miss out the links. Indeed what we actually see is that if the links are noted well the rest of the idea can be summarised in just a few strokes of the pen.A. Noting links becomes very simple if we use the key words that follow. (Over time this will become automatic.)as, why and that is because, this is the reason why, since, given the fact that, (in some instances) given that; to convey explanation.tho although, despite the fact that; to convey oppositionbut on the other hand, but, nevertheless, however; to convey limitationsif it is possible that, assuming that; to convey supposition.as to as far as x is concerned, on the matter of; to convey referencetfe therefore, one can then conclude; to convey conclusion.The three symbols below (which can also be found in Part 2) are also extremely useful. =the same goes for, one might say the same of; to convey the idea ofequality or correspondanceon the other hand, contrary to; to convey the idea of difference or lackof correspondancein + in addition, furthermore, if we also take account of; to convey the ideaof additional precision.5Again the ‘e’ represents the French feminine ending. Any letter can be used and this will depend on the languages involved.B. Linking is not just about representing the idea; it will often impacton the very content of the speech. It is a question of notingquickly and without repetition the group of subject words and thegroup of complement words to which the idea relates. This problemcan be solved quickly and easily by using the the recall arrow (JeanHerbert)Examine carefully the examples of links in Part 3.4. and5. Negation and emphasisNegation and emphasis are two essential elements of any speech and as such should be noted unambiguously (See Jean Herbert pp46-47).1. NEGATIONNegation might be noted by means of a line running through a word or symbol. Example:If we use OK to signify …agree”, then …disagree” will be OK . It is also possible to write the word no before the word to be negated (thus in our example we would note no OK). This second method is clearer and since …no” is a very short word using it is not a problem.2. EMPHASISTo emphasize a word we can underline it (twice if we are dealing with a superlative or absolute).Example:…(The study) is interesting” : int g…(The study) is very interesting” : int g…(The study) is extremely interesting” : int gIn some cases the line may be replaced by a circumflex to avoid confusion arising from the use of verticality.Alternatively emphasis can be noted with a dotted line.Example:…This report might be useful” : usefulThe use of underlining to denote nuance allows us to qualify the word (or idea) underlined without noting the qualifier.Example:…important question” becomes : ?…we should look at this very carefully” becomes : look at…I would like to say in the strongest possible terms” becomes : I say…...an imperfect solution” becomes : sol tn6. VERTICALITYIt is the principles of Verticality and Shift (described in the next section) which form the backbone of the note-taking system described in this book.Verticality means taking notes from top to bottom rather than from left to right. This method makes it possible to:a) group ideas logically, allowing a complete and immediate synthesis when we come to read back our notes,b) to do away with many links which would otherwise be essential to the clarity of the text.A. STACKING…Stacking6” consists of placing different elements of the text above or below one another.…the report on western europe”R ort .W Eur.…the report on western europe is an interesting document”R ort int gW Eur.…Since the French, US and UK delegations....”…Since the French, US and UK delegations have suggested....”FreAs USUKFreAs US suggest dUK…T he chapters of the report which deal with economic situation in Europe offer additional information and new statistics”Ch rs info_________ give newEc.Eur stat ics6…Superposition” in FrenchIf (as we will see in part 2) the sign → is used to denote …offer” and the sign + to denote …additional” and …new” then our notes will look like this:Ch rs info_________ → +Ec.Eur stat icsSee the examples in the practical exercises in part 3 and study them carefully.B. USING BRACKETSBrackets are an important part of the verticality system. In every speech there will be certain elements, which are mentioned to clarify an idea or to highlight a particular point, but which are not integral to the speaker’s train of thought.These parts of a speech should be noted in brackets, below the main element to which they refer.Examples:…....which leads to new investment, particularly in the transport sector”→ + inv ts(T ort)…(We hear that our exports will suffer as a result of increases in factor costs), which will make them less competitive.”(so - comp ive)See also the examples of the use of parentheses given in the practical exercises at the back.To encourage a natural use of the verticality technique it is recommended that you use relatively large but narrow pieces of paper. This will allow you to note the maximum amount of text on one page whilst automatically bringing your notes back to the left hand side of the page.7. SHIFTShift and Verticality are the fundamental principles underlying this note-taking system.To explain Shift let us take an example: …Over the course of 1954, prices rose, although not to the same extent as income, thus the population’s net income increased.” Our notes will be as follows ( the symbol ⌦ denotes increase):54, prices ⌦but ───── no = ⌦ incomeso ────Pop on⌦Word for word on the first line : Over the course of 1954, prices rose,Word for word on the second line : although not to the same extent as income,Word for word on the third line : thus the population’s net income increased.Having used Shift to give our notes a vertical layout on the page, noting the links is almost enough to give us an accurate and full version of the text.Shift means writing notes in the place on a lower line where they would have appeared had the text on the line above been repeated.The examples below show how notes would be positioned during interpretation, but have not been abbreviated.…The report on the economic situation in Europe is a fine document which discusses some interesting topics”:R ort goodEc.Eurdiscusses interesting topics…to understand the program, one must”to understand the programone must…The effectiveness of the Social and Economic Council’s efforts at solving.....”effectiveness efforts Ecosocat solving.....…Thus in the Report and the Study we find a theoretical and practical analysis which will help in the adoption of......”tfe(in R ort)Studytheoreticalthere is analysis practicalwhich will help in the adoption of See also examples of Shift in part 3.。

He is an outstanding individual,and there are several reasons that contribute to his excellence in English.Firstly,he has a strong passion for the English language.This passion drives him to immerse himself in the language,reading extensively,and engaging in conversations with native speakers whenever possible.His enthusiasm for learning is infectious and motivates others around him to improve their language skills as well.Secondly,he possesses excellent study habits.He allocates specific time each day to practice English,focusing on different aspects such as grammar,vocabulary,listening, speaking,reading,and writing.He also uses various resources,including textbooks, online courses,mobile apps,and language exchange programs,to enhance his learning experience.Thirdly,he is highly disciplined and consistent in his approach to learning.He sets clear goals for himself and works diligently to achieve them.He tracks his progress and adjusts his study plan accordingly to ensure continuous improvement.Moreover,he actively participates in English language activities and events.He joins English clubs,attends seminars,and takes part in debates and public speaking competitions.These experiences not only help him improve his language skills but also boost his confidence and communication abilities.Additionally,he is open to feedback and constantly seeks to learn from his mistakes.He values constructive criticism from teachers and peers and uses it as an opportunity for growth.He also reviews his work and identifies areas that need improvement. Furthermore,he has a strong foundation in English grammar and vocabulary.He has spent considerable time mastering the basics,which allows him to communicate effectively and understand complex texts.His extensive vocabulary enables him to express his thoughts precisely and engage in nuanced discussions.Lastly,he has a natural aptitude for languages,which makes learning English easier for him.However,he understands that talent alone is not enough and complements it with hard work and dedication.In conclusion,his excellence in English is a result of his passion,disciplined study habits, active participation in languagerelated activities,openness to feedback,strong foundation in grammar and vocabulary,and natural language aptitude.His commitment tocontinuous learning and improvement sets him apart and makes him an exemplary English learner.。

毕业英语论文范文毕业论文(设计)质量是衡量高等职业院校办学成果最为重要的依据之一,也是评价一个学生综合素质的重要标尺。

下面是小编为大家推荐的毕业英语论文范文，供大家参考。

毕业英语论文范文范文一：商务英语毕业论文Implication of Cultural Differences on International Business NegotiationsAbstractBusiness negotiations under different cultural conditions are cultural negotiations. With the development of economic globalization and frequent business contacts，cultural differences havebecome very important. If they are neglected， they could cause unnecessary misunderstanding，or even undermine the result of business negations. Therefore， it is of great significance to know different cultures of different countries as well as ways to avoid cultural conflicts in the context of international business negotiations. The paper begins with the definition of culture，analyzes the causes of cultural differences and explains the impact of cultural differences on international business negotiations from three perspectives of communication process，negotiation style and values concept. Finally，it analyzes effective ways to deal with the problem arising from cultural differences in the negotiation process. The paper stresses that in business negotiations between different countries negotiators should accept the other party's culture， try to make him be accepted and make a correct evaluation with help of effective communications. In a word，for successful cultural negotiations，cultural differences need to be perceived，accepted and most importantly played down.Key words:culture cultural difference business negotiation impactContents1. Cultural difference (4)1.1 The definition of culture (4)1.2 The causes of cultural differences (4)1.2.1 Geographical differences (4)1.2.2 Ethnic differences (4)1.2.3 Political differences (4)1.2.4 Economic differences (4)1.2.5 Religious differences (4)1.2.6 The concept of difference (5)1.3 Importance of international business negotiations on Cultural differences (5)2. Cultural differences on the impact of international business negotiations (5)2.1 Communication process (5)2.2 Negotiating style (8)2.3 Values (8)2.3.1 Ethics (8)2.3.2 Sense.............................................................................. (8)2.3.3 Concept of Collective (8)2.3.4 Concept of time (8)3. How to deal with international business negotiations and culturaldifferenc es (9)3.1 To learn more about the former in the negotiations of the cultural differences that may arise (9)3.2 In the negotiations necessary to correctly handle the cultural differences (9)3.3 Negotiations to do a good job of follow-up for the exchange of cultural differences (10)4. References (11)Business negotiation in interpersonal relationships as a special form， relate to different geographical， ethnic， social and cultural exchanges and contacts， which have taken place in cross-cultural negotiations. In cross-cultural negotiations，the different geographical， ethnic， cultural differences will affect the thinking of those negotiations，the negotiation style and behavior，thus affecting the entire negotiation process. Therefore， to engage in business activities， especially for the cross-border business activities must understand and master the links between different cultures and differences. Conducting negotiations with the organization，also have to understandthat cultural differences impact on the negotiations， only the face of such a positive impact on the desired objectives can be achieved1. Cultural differences1.1 the definition of cultureNational culture is a country-specific concepts and value systems，which constitute the concept of people's lives and work behavior. The nations of the world as a result of specific historical and geographical and gradually formed its own unique cultural traditions and cultural patterns. As the difference of Chinese and Western traditional customs，values，religious beliefs ， different ways of thinking， etc， making the different performance of Chinese and Western cultures.1.2 the causes of cultural differencesCultural diversity caused by many reasons， T o sum up， the main source of cultural differences are in the following areas:1.2.1 geographical differencesRefers to the geographical differences in different geographic regions due to the geographical environment， the level of economic development and traditional differences in habits，people often have different language，lifestyle and hobbies. And these will affect their behavior. For example， the West and the American people in some countries treat Christmas important， but in areas such as near the equator do not have snow all the year round， the people of some African countries may not have the concept of Christmas because the best modified Christmas is snow， as to the people in the region that are not long-term snow ，there is little concentration of Christmas than American States.1.2.2 national differencesEthnic differences is the different ethnic groups in the development of long-term process， the formation of their own language，customs and preferences，habits. Their diet，clothing，accommodation，festivals and rituals，such as material and cultural life of their own characteristics. Take the history of our country and our Hun Han， the Xiongnu people are valiant， characteristics of typical nomads. And we tame the Han character，the typical characteristics of farming nation. Which led to the Huns in the diet， clothing， accommodation，festivals and rituals，such as material and cultural life are different with Han.1.2.3 the political differencesPolitical differences are due to the political system and the policies and regulations on people's behavior with the role of a standardized， so that all peoples in the political aspects on the concept of the existence are differences. Take the United States and France as example， the United States by the Constitution the powers of the President of the severe restrictions on the two major powers with other institutions of Congress and the Supreme Court of strong constraints. While France also had to set was ready to royalist restoration of the monarchy of the Third Republic to amend the Constitution a little further expand the powers of the president.1.2.4 economic disparitiesEconomic differences are result of the economic factors of a reflection of cultural differences. For example， the people in the Western developed countries are rich lives and high level of education， people will pay more attention to the quality of life，security means more generally. And economic backwardness of the Third World， people care more about food and clothing.1.2.5 religious differencesReligion is the development of human society to a certain stage of historical phenomenon， Religion has its own (Catholic) Major epidemic in Western Europe and South American; Islam is the scope of the whole of the Middle East and North Africa. Buddhism is more prevalent in Asian countries. The world has three major religions: Christianity，Buddhism and Islam. Christian (Protestant) is major epidemic in Northern Europe，North America and Australia; people in many parts of Asia believe in Buddhist. Different religions have different cultural tendencies and precepts，which affect the way of people understand things， codes of conduct and values.1.2.6 the concept of Values differenceValues are means of objective evaluation criteria of things. It includes the concept of time， wealth， the attitude towards life，the attitude to risk and so on. Different societies’ people to the same things and problems will come to different and even opposite conclusions.Geographical differences，ethnic differences，political differences，economic differences，religious differences and differences in concepts have the impact on people's penetration in the food， clothing， accommodation， festivals and rituals，such as material and cultural life in all its aspects. Thus affecting people's behavior，values，religious beliefs and modes of thought have a lot of difference， Finally has formed the various countries and areas of cultural differences.1.3 cultural differences on the importance of international business negotiationsPractice in the negotiations， many negotiators often do not understand，or took note of the cultural importance of thesignificant impact on negotiations. Negotiating parties for foreign culture，some negotiators may have noticed some of the other negotiations， "different" or "hard to understand" the concrete manifestation of negotiations，but that is not important. Some people blindly believe that negotiation is the use of foreign-related facts and figures to speak， and the facts and data are common. Similarly，some foreign countries’ negotiators to negotiations with each other to maintain harmonious relations， they will notice the similarities between both cultures， while ignoring their differences. Let's look at an example.In 1992，negotiators from China and other 12 experts of different professions to form a delegation to the United States purchases about 30 million U.S. dollars of chemical equipment and technology. The US naturally does everything possible to satisfy them. One of them is negotiations in the first round of the delegation sent to each of them a small souvenir. The Souvenirs packaging is very particular is a beautiful red box，red for advanced. But when the delegation was pleased to open the box when face-to-face in accordance with the Americans，Everyone's face appears very not the nature actually--there is a golf cap，but the color is green. American businessman's intention is: after signing the contract，and everyone to play golf. But they don’t know the "be a cuckold" is the biggest taboo in Chinese men. Finally the delegation did not sign the contract，not because the Americans "insult" people，but because they work careless，and even don’t know the common sense that Chinese men taboo "be a cuckold". How can we feel free to tens of millions of dollars project to them? It can be seen that the failure of the Americans negotiation is due tothey do not understand the Chinese culture.From the above examples，we can learn in business negotiations，if we do not attach importance to each other's cultural differences， the negotiations are likely to lead to failure.2. Cultural differences on the impact of international business negotiationsThe impact of culture on negotiations is extensive and profound，and different cultures will naturally divided people into different groups， this region， the difference between their respective groups are bringing people of different cultural groups tend to alienate each other; On the other hand， different cultural communication and exchanges between people are also obstacles. Therefore，the requirements of the negotiators to accept each other's culture， but also by cultural differences，unmistakably reveals that the purpose of understanding of each other's behavior，and they have been accepted by the other party， and ultimately reach a consensus agreement.Overall， the impact on culture negotiations are in following several aspects:2.1 the communication processCultural differences on the communication process of the negotiations，first of all is the performance of the communication language in the negotiation process. Language is a bridge of any country， any region and any nation. States companies， individuals to conduct business negotiations， we must first have the language to this. The differences language of international business activities is the most direct and clear. Such as China's "white elephant" brand batteries，to the English "White Elephant" it would cause bad associations.Because the "White Elephant" In addition to the name ofanimals that have two meanings: "The owner did not use， but may be useful to others; do not reuse things." Solve the language problem is very simple，you can hire a translator or use a common third language to talk. While the negotiators of the language used in a variety of cultures with higher fitness， but no matter what， the difference is obvious. Such as Japan， Brazil and France Culture，the Japanese style of business communication is the most polite， more positive commitment to the use of recommended and guarantees，and less use of threats， commands and warnings of freedom of speech， their manners of speech style， The most prominent is that they do not often use "no"， "you" and facial gaze， but to maintain a period of silence; Brazilian businessmen to use "no" and "you" at the higher frequency，their negotiation style seems more presumptuous， and it seems not lonely in the negotiations， to gaze at each other and touch each other from time to time; French businessmen negotiating style is all the most presumptuous， in particular， their use of threats and warnings at the highest frequency，in addition，they are still very frequent use of interrupted， facial gaze， as well as "no" and "you". It can be seen， only to clarify these differences that can avoid the reticent Japanese，Brazilian over enthusiasm or the French’s misunderstanding of the threat， which achieved the success of international business negotiations.Cultural differences impact on the negotiation process not only in the process of language communication， but also in the process of non-verbal communication. Cultural differences will lead to different countries or regions in the body language of negotiations， the use of action language significantly different，or even the same language of action is diametrically opposed tothe transfer of information. For example， the vast majority of countries are in favor of nod his head for agree. But in India，Nepal and other countries that are certainly shaking his head，that is， shaking his head and smiling， that is positive meaning，some people just do it diagonally on the rise is still a good way，some people are a population frequency said "You are right! You are right!" but a continuously shaking his head，often make others do not know its true psychological and full of doubt. But negotiators shape， movement， language， awareness and use of the differences， also create an obstacle for the negotiations in communication.Cultural differences also can lead to the negotiators of the differences in communication. People of different cultures have their preferences and habits of communication and cross-cultural negotiations in the negotiating parties often belong to different cultures， have their own customary means of communication. Accustomed to different means of communication between the parties to conduct a more depth in communication， often cause a wide range of issues. From countries with a high culture of the negotiators and those from countries with low culture of the negotiators may be in different ways of expression during the negotiation process. From countries with a high culture of the negotiators may be chosen euphemism，indirect ways to express their meaning. While from low culture of the negotiators preference for using oral expression to negotiate，direct or receive a clear message，straightforward means to express themselves. These two negotiators from different cultures during the negotiations，the party think the other side is often too rough，while the other may think that the other side lack of good faith in negotiations， or misunderstanding the silence ofeach other's conditions for its approval.2.2 the negotiation styleThe negotiation style is the main bearing and the attitude which displays in the negotiations activities. the style of negotiations in the course of negotiators’ behavior， conduct and control of the negotiation process of the method and means. Negotiators negotiations Style with a deep cultural stigma. Culture not only determines the Ethics Code of Ethics for negotiators，but also affects the way of thinking negotiators’ behavior and personality，so that make the negotiators of different cultural backgrounds form a very different style of negotiation. Negotiating style of the negotiation process for the negotiations between the two sides approach the relationship，contacts， and even the structure of the negotiations has a direct impact.Adhere to cultural differences，negotiating styles can be divided into two types: the negotiation style of Oriental and Western style negotiations. Oriental style is based on negotiations as the background of oriental culture of Asian countries negotiation styles，with Japan，South Korea for a typical representative:Japanese business men are conservative，attention to status-oriented，credit and the initial cooperation，co-dependent relationship between stress and good at negotiating. Japanese attached great importance to the negotiations in the transaction to establish harmonious interpersonal relationships. If there had been contacts with Japanese，before the negotiations should be recall the past exchanges and friendship between the two sides，which will be beneficial to the next negotiations. They did not support and habit the direct， purelycommercial activities. If it is the first time to establish trade relations with Japanese， the party responsible for higher status in charge visits in opposite party enterprise at the same level status person in charge is extremely important，it attached great importance to Japanese companies and the trading relationship with you. When negotiations with Japan，it’s the best to send staff rank and status at high-level than the other side. This will facilitate the conduct of the talks. It should also be noted that Japanese women's status in society is lower，generally they not allowed to participate in the operation and management of large companies activities，the Japanese are also in a number of important occasions of non-female. Therefore， when encountered formal negotiations generally not appropriate to allow women to participate in， or else they may be skeptical， and even expressed dissatisfaction.Korean character stubborn， often stuck to their own views in the negotiations and will not easily compromise. In this case we must grasp the strategy， it is necessary to adhere to argue，but also common sense to master a certain sense of propriety，and sometimes also need to be patient. On the other hand，South Korea in the negotiations seldom to express the views directly， often need the other side to try to figure out， in order to accurately understand the meaning of each other，South Korea may ask the same question repeatedly，so that when making decisions to ensure the correctness. And South Korea signed a contract does not mean that their success will not be changed， for other reasons they would seek to amend or re-start negotiations with you.Western-type style of negotiation is based on Western culture of Europe and the United States as the background styleof negotiations. The main representatives are the United States and United Kingdom.Americans often talk about "Business is Business" (business to the business) means doing business need to not recognize one's own closest relatives， insist on the principle of things not for people. "Time is money"，"money is everything" is the unswerving credo of American. Their business activities is often straightforward，be anxious for success，business came straight to the point， they always picking up the phone to talk，sit down and get straight to the point，They calculate the progress by the hour and the number of days， their opponents often feel pressure from them. American businessmen do not like the use an agent or participate in negotiations with the consultant，give others the impression that they can say on behalf of the company. They like to sit down to do business immediately. In addition，the United States businessmen attached great importance to economic benefits， they have a slang called: "Bang for Buck"， that is， with minimum capital investment to obtain the greatest benefit.British merchants engaged in commercial activities pay more attention to informal traders than other countries in the world，but also more conservative. Even today， the world has entered the electronic information age， in the UK by telephone to talk about business is unacceptable. British businessmen are more willing to make full preparations in advance， and then face-to-face talks. As long as they do not believe that the details of a settlement will not solve， they will never sign， all must have to do as rule. As a result of the British very great importance to the position， the title is also very important to them. Therefore，the selection status of the person as a broker of highly influentialbusiness，political forces and the role of trade unions in the business also can not be neglected.Of course，it also must pay attention to the actual negotiations process， although the same cultural background of the negotiators， the talks there was a clear difference， but subject to sub-culture，as well as other factors，the same cultural background of individual negotiators， the negotiations style can be very different.2.3 Cultural valuesCultural values is measure the consequences of people's behavior and standards. They affecting the way of people understanding the problems and will give rise to a strong emotional impact. In different cultures，values will be very different. Culture in a very appropriate behavior in another culture may be seen as immoral. For example，Americans believe that nepotism is immoral， however it as an obligation at the majority of Latin American culture. Therefore，the Understanding of a certain society in popular as well as these ideas in the personal behavior the degree which respects is very important. Our discussions here will focus on those activities is essential to understand the socio-economic values，more specifically，is these for promote the cross-cultural communicative competence and the values is worth noting.2.3.1 EthicsChina has heavier ethics. "Acquaintance" and "relationship" has its own special meaning and significance， once the relations have been established，the two sides have become acquaintances or friends， and generous concessions to help the situation appear， and the degree of trust and tolerance will be improved，so the Chinese people have more oral agreement.Americans is not the case，they do not pay attention to cultivating the feelings of both sides， and attempts to separate business and friendship. To deal with the problem， often used the legal means， lawyers come forward to solve the problem is common，it is flexible and not rigid，we should clearly recognize this point. However，once sign the contract，they are very much focused on the legal contract， the performance of the contract is higher. The Chinese delegation to the West，maybe a long time no one could entertain，and this misunderstanding of the people are not interested in their visit; Europeans come to China， No matter what they do may find that there are people who accompanied，and this misunderstanding of the people lack of trust in them. Of foreign visitors， a senior care too much， not to mention dinner， often mistakenly believe that this expressed his company's products or have a preference， this in fact is the Chinese hospitality， This can lead to subsequent disappointment， and even complain.2.3.2group awarenessIn the course of the Chinese and Western cultural traditions and different cultural values， on the negotiations issues tend to have a confrontation or misunderstanding. China's national character has a very remarkable phenomenon， that is Settles on the face or the dignity. At the negotiating table， if make a choice from "decent" and "interest"， both the Chinese people will often choose to "decent." Why do the Chinese people want to save face at all costs? Because of the ideological core of Chinese culture is a group consciousness. In accordance with the sense that each one is not a separate person，but living in a certain social relations， and no face will not the face of others， there is no face on the people and will not be able to live in the social andgroup life，and may even be abandoned by society and the groups. But not like Westerners，they value the interests of negotiations，they will not hesitate to choose interest from "decent" and "interest" of the two. Chinese people regarding negotiations result whether can bring honor for their face， looks extremely important，as well as some Western negotiators in their works cautioned China in the talks， we must note that use of China's national character. It is clear that only a correct understanding and properly grasp the existence of Chinese and Western differences in national character， can effectively help us in a timely manner to correct our own shortcomings and strengthen our own advantages and use of other's shortcomings to collapse of other's strengths.2.3.3 the concept of collectiveChina's concept of collective a stronger emphasis on collective responsibility，Therefore the negotiations pattern basically is the collective， but to make the final decisions are a decisive one， and even the decisive one simply has not entered the stage. This is known as the cultural experts of "high from the right to culture"，in the event of difficult issues more complicated， the negotiators on the difficult decisions; and the Western culture of Jurists which was referred to as "low from the right to culture"，on the surface is one or two people out，negotiators have been given the appropriate permissions，or assisted in its decision-making think-tank，which in the negotiations，the sole responsibility of the negotiations were heavier， higher and more flexible.2.3.4 the concept of timeConcept of time and how it decided the people's action plan for international business negotiations has a broad impact of theinvisible. The daily negotiations behavior manifests observes the difference aspect of time may be is the most obvious results of the performance. Jewish businessmen attached great importance of time. They always believe that time is not money， time and goods， is the capital to make money. Money can borrow， but time can not be borrowed，the time is more valuable than money. A wealthy Jewish income of 200，000 US dollars monthly have been considered such an account: his daily wage is 8 1000 U.S dollars，then about 17 U.S. dollars per minute. If he had been disturbed and waste 5 minutes， then is the equivalent of stolen 85 U.S. dollars in cash. Strong concept of time improved the efficiency of the Jews， they are often at work in seconds and every second counts. On the Jewish people， never appear leave early，late，or to stall for time and so on. In the business activities of the Jews "Uninvited guest" is almost as the same as the “unwelcome person”，because uninvited guests will disrupt the timing of the original， and waste everybody's time. For the time extremely mean of the Jewish，in the time to discuss the concept of time is stronger. Before Jews in the negotiations， the time must have been agreement. They agreed not only in a certain period of a day，but also appointment "from the starting points to a few minutes to talk about." During the meeting， in addition to polite greetings outside， the Jews immediately to discuss business， this is have good manners and good performance， at the same time that mean respect of each other.3. how to deal with the cultural differences on international business negotiationsOnly recognize and accommodate cultural differences can take the whole process of negotiations in response to。

《英语语言学概论》配套练习题（二）（判断题）Chapter 1 An Introduction to Linguistics1. Duality is one of the charateristics of human language. It refers to the fact that language has two levels of structures: the system of sounds and the system of meanings.2. Prescriptive linguistics is more popular than descriptive linguistics, because it can tell us how to speak correct language.3. Competence and performance refer respectively to a language user’s underlying knowledge about the system of rules and the actual use of language in concrete situations.4. Arbitrariness of language makes it potentially creative, and conventionality of language makes a language be passed from generation to generation. As a foreign language learner, the latter is more important for us.5. By diachronic study we mean to study the changes and development of language.6. Langue is relatively stable and systematic while parole is subject to personal and situational constraints.7. Language change is universal, ongoing and arbitrary.8. Applied linguistics is the application of linguistic principles and theories to language teaching and learning.Chapter 2 Phonology1. Of the three phonetics branches, the longest established one, and until recently the most highly developed, is acoustic phonetics.2. Sound [p] in the word “spit” is an unaspirated stop.3. The airstream provided by the lungs has to undergo a number of modificaiton to acquire the quality of a speech sound.4. [p] is voiced bilabial stop.5. Acoustic phonetics is concerned with the perception of speech sounds.6. When pure or monophthongs are pronounced, no vowel glides take place.7. According to the length or tenseness of the pronunciation, vowels can be divided into tense vs. lax or long vs. short.8. Received Pronunciation is the pronunciation accepted by most people. Chapter 3 Morphology1. Phonetically, the stress of a compound always falls on the first element, while the second element receives secondary stress.2. Fore as in foretell is both a prefix and a bound morpheme.3. Base refers to the part of word that remains when all infletional affixes are removed.4. In most cases, prefixes change the meaning of the base whereas suffixes change the word-class of the base.5.Conversion from noun to verb is the most productive process of conversion.6. The word, whimper, whisper and whistle are formed in the way of onomapoeia.7. Backformation is a productive way of forming nouns in Modern English.8. All roots are free and all affixes are bound.Chapter 4 Syntax1. Application of the transformational rules yields deep strucutre.2. Move-a rule itself can rule out ungrammatical forms and result in grammatical strings.3. Number and gender are categories of noun and pronounn.4. A constituent which is not at the same time a construction is a morpheme, and a construction which is not at the same time a constituent is a sentence.5. IC analysis can be used to analyze all kinds of ambiguous structures.6. A sentence contains a point of departure and a goal of diacourse.7. Syntactic category refers to all phrasal syntactic categories such as NP, VP, and PP, and word-level syntactic categories that serve as heads of phrasal syntactic categories such as N and V.8. S-structure is a level of syntactic representation after the operation of necessary syntactic movement.Chapter 5 Semantics1.Interrogative and imperative sentences do not have truth value.2.The raltionship between “human body” and “face/nose” is hyponymy.ponential analysis is based on the belief that the meaning of a word cannot be dissected into menaing components, called semantic features.4.One merit of componential analysis is that by specifying the semantic features of certain words, it will be possible to show how these words are related in meaning.5.Hyponymy is a matter of class membership, so it is the same as meronymy.6.“Either it is raining here or it isn’t raining here” is empirically true.7.Two sentences using the same words may mean quite differently.8.Linguistic forms having the same sense may have different references in different situations while linguistic forms with the same reference always have the same sense. Chapter 6 Pragmatics1.If the context of use is considered, the study is being carried out in the area of pragmatics.2. A locutionary act is the act of expressing the speaker’s intention.3.When performing an illocutionary act of representative, the speaker is making a statement or giving a description which he himself believes to be true.4.The utterance meaning of the sentence variees with the context in which it is uttered.5.While conversation participants nearly always observe the CP, they do not always observe these maxims strictly.6.Inviting, suggesting, warnign, ordering are instances of commissives.7.Only when a maxim under Cooperative Principle is blatantly violated and thehearer knows that it is being violated do conversational implications arise.8.Of three speech acts, linguists are most interested in the illocutionary act because this kind of speech is identical with the speaker’s intention.Chapter 7 Language Change1.Pre-Indo-European languages are not attested whereas Proto-Indo-Europeanlanguages are attested.2.Some modern words come from the morphological change of the Old English. Forinstance, move comes form movement and teach comes from teachable.3.With the semantic broadening or narrowing, the meaning of a word is beingchanged constantly, although with one generation such difference is hardly obvious.4.The sentence I hate thee not was considered normal form of negation in OldEnglish.5.Both Chinese and Japanese have a logographic writing system; English and Greekhave an alphabetic writing system.6.In Old English, the affixation of the prefix Y an- to an adjective would change theword into a causative verb.7.In 1200, the official language in England was Old English.8.All case forms of Old English nouns have been lost in Modern English.9.In Old English, a verb precedes the subject instead of following it. Chapter 8 Language and Society10.In most bilingual communities, two languages have the same in speech situatio nsknown as domains.11.A regional variety of a language is intrinsically inferior to the standard variety ofthat language.12.A pidgin is not a native language of a particular region.13.When a bilingual speaker switches between the two languages concerned, he isconverting one mode of thinking into the other.14.Pidgins are rule-governed, like any human language.15.According to the strong version of the Sapir-Shorf hypothesis, speaker’sperceptions determine language and pattern their way of life.16.The sentences “He crazy”and “He be sick all the time”are both acceptible inblack English vernacular because copula deletion and habitual be are two famous of black English.17.There are words of more or less the same menaing used in different regionaldialects.Chapter 10-11 Language Acquisitionnguage use is both systematic and non-systematic, subject to external as well as to internal variation.2.In linguistic study, linguists first work out a theory about language structure, then, test it with language facts.3.Formal instruction hardly affects the natural route of SLA.4.If language learners are provided with sufficient and the right kind of language exposure and chances to interact with language input, they will acquire the native-like competence in the target language.5.Phonologically slower rate of delivery is an example of conversational modification.6.Children’s grammar develops gradually until it becomes exactly the adult’s grammar.7.Foreinger talk is always ungrammatical.8.Learners with different first languages would learn a second language in differnet ways.Chapter 12 Language and Brain1. The right ear advantage (REA) is true no matter whether people have the left hemispheric dominance for speech or the less common right hemispheric dominance.2. In general, the left hemisphere controls voluntary movements of, and responds to signals from, the right side of the body.3. The left hemisphere is superior to the right hemisphere.4. Although the age at which children will pass through a given stage can vary significantly from child to child, the particular sequence of stages seems to be the same for all children acquiring a given language.5. At the multiword stage, simple prepositions, especially those that indicate positions such as “in”, “on” and “up”, begin to turn up in children’s speech.6. Children acquiring their first language simply beyond the critical age are hardly successful, such as the case of “Genie.”7. In first language acquisition children’s grammar models exactly after the grammar of adult language.8. Modern linguists regard the spoken language as primary, not the written.。

语言学第五版第六单元术语1. Psycholinguistics is the study of psychological aspects of language; it usually studies the psychological states and mental activity associated with the use of language. As an interdisciplinary academic field basied on psychology and linguistics, psycholinguistics investigates the six following subjects: language acquisition, language comprehension, language production, language disorders,language and thought, and cognitive architecture of language, the most important research subjects are acquisition, comprehension and production.2. Language acquisition is one of the central topics in psycholinguistics. Acquiring a first language is something every child does successfully, in a matter of a few years and without the need for formal lessons. Four phrases are identified and acknowledged in the process of language acquisition: holophrastic stage, two word stage, three word utterances, and, fluent grammatical conversation stage.3. holophrastic stage is the first phase of language acquisition. The main linguistic accomplishments during this stage are control of the speech musculature and sensitivity tothe phonetic distinctions used in the parents’language. Shortly before their first birthday, babies begin to unstand words, and around that birthday, they start to produce them.4. two word stage is the second phase of language acquisition. Around 18 months, the child begins to learn words at the rate of one every two walking hours, and keeps learning that rate or faster through adolescence.5. Three word utterances stage is the third phase of language acquisition. Three word utterances look like samples drawn from longer potential sentences expressing a complete and more complated idea.6. connectionism: With respection to the respect to language comprehension, connectionism in psycholinguistics claims that readers use the same system of links between spelling units and sound units to generate the pronunciations of written words and to access the pronunciations of familiar words, or words that are exceptions to these patterns. In this view, similarity and frequency play important roles in processing and comprehending language, with the novel iterms being processed based on their similarity to known ones.7. Cohort model is a supposed doctrine dealing with the spoken word recognitionpostulation postulated by Marslen Wilson and Welsh in 1990. It is suggested that the first few phonemes of a spoken word activate a set or cohort of word candidates that are consistent with the input. These candidates compete with one another for activation. As more acoustic input is analyzed, candidates that are no longer consistent with the input drop out of the set. This process continues until only one word candidate is a clear winner.8. Interactive model holds that in recognizing the spoken words higher processing levels have direct, “top down”influence on lower levels. Lexical knowedge can affect the perception of phonemes. There is interactivity in the formal of lexical effects on the perception of sublexical units. In certain cases, listeners’ knowledge of words can lead to the inhibition of certain phonems; in other cases, listeners continue to “hear” phonemes that have been removed from the speech signal and replaced by noise.9. Race model suggests in spoken word recognition there are two routes that race each other a pre lexical route, which computers phonological information from the acoustic signal, and a lexical route in which the phonological information associated with a word becomes available when the word itselfis accessed When word level information appears to affect a lower level process, it is assumed that the lexical route won the race.10. Serial model proposes that the sentence comprehension system continually and sequentially follows the constraints of a language grammar with remarkable speed. serial model describes how the processor quickly constructs one or more representations of a sentence based on a restricted range of information that is guaranteed to be relevant to its interpretation ,primarily grammatical information .Any such representation is then quickly interpreted and evaluated, using the full range of information that might be relevant.11. Parallel model emphasizes that the comprehension system is sensitive to a vast range of information .including grammatical, lexical, and contextual, as well as knowledge of the speaker writer and of the world in general. parallel model describes how the processor users all relevant information to quickly evaluate the full range of possible interpretations of a sentence .it is generally acknowledged that listener and readers integrate and situational knowledge in understandinga sentence.12. Resonance model is a model about text comprehension,in this model , information in long term memory is automatically activated by the presence of material that apparently bears a rough semantic relation to it .semantic details, including factors such as negation that drastically change the truth of propositions , do not seem to affect the resonance process. It emphasized a more active and intelligent search for meaning as the basis by which a reader discovers the conceptual structure of a discourse. In reading a narrative text, reader attempts to build a representation of the causal structure of the text. analyzing events in terms of goals ,actions, and reactions .A resonance process serves as first stage in processing a text, and , reading objectives and details of text structure determine whatever a reader goes further searches for a coherent structure for the text.13. Construal is the ability to conceive and portray the same situation inalternate ways through specificity, different mental scanning, directionality, vantage point, figure ground segregation etc.14. Construal operations are conceptualizing processes used in language process by human beings. That is, construal operations are the underlying psychological processes and resources employed in the interpretation of linguisticexpressions.15. Figure ground alignment seems to apply to space with the ground as the prepositional object and the preposition expressing the spatial relation configuration. It also applies to human perception of moving object. Since the moving object is typically the most prominent one, because it is moving, it is typically the figure, while the remaining stimuli constitute the ground.16. Trajector means a moving or dynamic figure.17. Landmark means the ground provided for a moving figure.18. Basic level category is the most economical level at which you can find the most relevant information. The information on our interactions with objects in the real world are stored at this level. It is at this level that we conjure up the gestalt of the category.19. Subordinate level is the level at which we perceive the differences between the members of the basic level categories.20. Image schema is a recurring, dynamic pattern of our perceptual interactions and motor programs that gives coherence and structure toour experience.21. Metaphor involves the comparison of two concepts in that one is construed in terms of the others. It’s oftendescribed in terms of a target domain and a source domain. The target domain is the experience being described by the metaphor and the source domain is the means that we use in order to describe the experience.22. Metonymy is a figure of speech that has to do with the substitution of the name of one thing for that of another.23. Ontological metaphors mean that human experiences with physical objects provide the basis for ways of viewing events, activities, emotions, ideas, etc., as entities and substances.24. Structural metaphors play the most important role because they allow us to go beyond orientation and referring and give us the possibility to structure one concept according to another.25. Generic space maps onto each of the inputs. It reflects some common, usually more abstuct, structure and organization shared by the inputs. It defines the core cross space mapping between them.26. Blend space is the fourth space onto which is partially projected by inputs I1 and I2。

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

几个逻辑相关的英语单词逻辑 logic数理逻辑 mathematical logic模型论 model theory集合论 set theory递归论 recursion theory证明论 proof theory非标准分析 nonstandard analysis反推数学 reverse mathematics元数学 metamathematics二阶算术的子系统 subsystems of the second-order arithmetic 直觉主义 intuitionism构造性数学 constructive mathematics语言 language元语言 metalanguage元定理 metatheorem公理 axiom定理 theorem命题 proposition命题演算 propositional calculus 谓词演算 predicate calculus合取 conjunction析取 disjunction非,否定 negation量词 quantifier全称量词 universal quantifier 存在量词 existential quantifier 关系 relation函数 function常量 constant变元,变量 variable项 term公式 formula原子公式 atomic formula句子,命题 sentence永真命题 tautology前束标准型 prenex normal form 理论 theory可满足的 satisfiable和谐性,相容性 consistency句法 syntax语义 semantics可靠性定理 soundness theorem完备性定理 completeness theorem 紧致性定理 compactness theorem可公理化 axiomatizable有限可公理化 finitely axiomatizable 同构 isomorphism同态 homomorphism初等等价 elementary equivalent 初等嵌入 elementary embedding 初等子模型 elementary submodel 初等扩张 elementary extension图象 diagram正图象 positive diagram初等图象 elementary diagram模型 model可数模型 countable model不可数模型 uncountable model原子模型 atomic model素模型 prime model齐性模型 homogeneous model万有模型 universal model饱和模型 saturated model特殊模型 special model递归饱和模型 recursively saturated model 布尔值模型 boolean-valued model格值模型 lattice-valued model超滤 ultrafilter超积 ultraproduct超幂 ultrapower模型完备 model complete子模型完备 submodel complete量词消去 quantifier elimination稳定性理论 stable theory集,集合 set子集 subset幂集 power set空集 empty set有限集 finite set无限集 infinite set可数集 countable set不可数集 uncountable set 有限集 finite set无限集 infinite set序数 ordinal极限序数 limit ordinal后继序数 successor ordinal 基数 cardinal大基数 large cardinal可测基数 measurable cardinal正则基数 regular cardinal奇异基数 singular cardinal不可达基数 inaccessible力迫法 forcing连续统假设 Continuum Hypothesis 选择公理 Axiom of Choice决定性公理 Axiom of Determinacy 归纳法 induction超限归纳法 transfinite induction 超限递归 transfinite recursion递归 recursion原始递归 primitive recursive递归函数 recursive function递归可枚举 recursively enumerable递归可判定 recursively decidable 递归不可分 recursively inseparable 递归集 recursive set算术集 arithmetical set解析集 analytic set单纯集 simple set创造集 creative set多一归约 many-one reducible一一归约 one-one reducible图灵归约 Turing reducible不可解度 degree of unsolvability 图灵度 Turing degree一阶逻辑 first-order logic二阶逻辑 second-order logic高阶逻辑 higher-order logic非古典逻辑 non-classical logic 无穷逻辑 infinitary logic古典逻辑 classical logic直觉主义逻辑 intuitionistic logic 模态逻辑 modal logic多值逻辑 many-valued logic。