A type-theoretic framework for formal reasoning with different logical foundations

A type-theoretic framework for formal reasoning

with di?erent logical foundations

Zhaohui Luo

Dept of Computer Science,Royal Holloway,Univ of London

Egham,Surrey TW200EX,U.K.

zhaohui@https://www.sodocs.net/doc/0416847490.html,

Abstract.A type-theoretic framework for formal reasoning with di?er-

ent logical foundations is introduced and studied.With logic-enriched

type theories formulated in a logical framework,it allows various log-

ical systems such as classical logic as well as intuitionistic logic to be

used e?ectively alongside inductive data types and type universes.This

provides an adequate basis for wider applications of type theory based

theorem proving technology.Two notions of set are introduced in the

framework and used in two case studies of classical reasoning:a predica-

tive one in the formalisation of Weyl’s predicative mathematics and an

impredicative one in the veri?cation of security protocols.

1Introduction

Dependent type theories,or type theories for short,are powerful calculi for logical reasoning that provide solid foundations for the associated theorem prov-ing technology as implemented in various‘proof assistants’.These type the-ories include Martin-L¨o f’s predicative type theory[NPS90,ML84],as imple-mented in ALF/Agda[MN94,Agd00]and NuPRL[C+86],and the impredicative type theories[CH88,Luo94],as implemented in Coq[Coq04]and Lego/Plastic [LP92,CL01].The proof assistants have been successfully used in formalisation of mathematics(e.g.,the formalisations in Coq of the four-colour theorem[Gon05]) and in reasoning about programs(e.g.,the analysis of security protocols).

The current type theories as found in the proof assistants are all based on intuitionistic logic.As a consequence,the type theory based proof assistants are so far mainly used for constructive reasoning.Examples that require or use other methods of reasoning,say classical reasoning,would have to be done by ‘extending’the underlying type theory with classical laws by brute force and praying for such an extension to be OK.

We believe that the type theory based theorem proving technology is not (and should not be)limited to constructive reasoning.In particular,it should adequately support classical reasoning as well as constructive reasoning.To this end,what one needs is a type-theoretic framework that supports the use of a This work is partially supported by the following research grants:UK EPSRC grant GR/R84092,Leverhulme Trust grant F/07537/AA and EU TYPES grant510996.

wider class of logical systems and,at the same time,keeps the power of type theory in formal reasoning such as inductive reasoning based on inductive types.

In this paper,we introduce such a type-theoretic framework where logic-enriched type theories are formulated in a logical framework such as LF[Luo94] and PAL+[Luo03].Logic-enriched type theories with intuitionistic logic have been proposed by Aczel and Gambino in studying type-theoretic interpretations of constructive set theory[AG02,GA06].They are studied here from the an-gle of supporting formal reasoning with di?erent logical foundations.We show that it is possible to provide a uniform framework so that type theories can be formulated properly to support di?erent methods of reasoning.The structure of our framework promotes a complete separation between logical propositions and data types.It provides an adequate support to classical inference as well as intuitionistic inference,in the presence of inductive types and type universes.

Two notions of set are introduced in the type-theoretic framework:a pred-icative one and an impredicative one.They are used in two case studies:one in the formalisation of Weyl’s predicative mathematics[Wey18,AL06]and the other in the formalisation and analysis of security protocols.Both case studies use classical reasoning–we have chosen to do so partly because how to use type theory in constructive reasoning has been extensively studied and partly because we want to show how classical logic can be employed in a type-theoretic setting.

The proof assistant Plastic[CL01]has been extended(in an easy and straight-forward way)by Paul Callaghan to implement the type-theoretic framework as described in this paper.The case studies have been done in the extended Plastic and help to demonstrate that type theory and the associated proof assistants can be used to support formal reasoning with di?erent logical foundations.

2Logic-enriched type theories in a logical framework

The type-theoretic framework formulates logic-enriched type theories(LTTs for short)in a logical framework.It consists of two parts,the part of logical proposi-tions and the part of data types.Both parts are formulated in a logical framework and linked by the induction rules(see below).

We start with the logical framework LF[Luo94]or PAL+[Luo03],where the kind T ype represents the world of types.Now,we extend the logical framework with a new kind P rop that stands for the world of logical propositions and,for every P:P rop,a kind P rf(P)of proofs of P.

The logic of an LTT is speci?ed in P rop by declaring constants for the log-ical operators and the associated rules(as logics are introduced in Edinburgh LF[HHP93]).The data types are introduced in T ype as in type theories such as Martin-L¨o f’s type theory[NPS90]and UTT[Luo94].Di?erent LTTs can be formulated in the framework for formal reasoning with di?erent logical foun-dations.Instead of considering LTTs in general,we shall present and study a typical example–the LTT with the classical?rst-order logic,abbreviated as LTT1,to illustrate how an LTT is formulated in our type-theoretic framework.

2.1LTT1:an example

The system LTT1consists of the classical?rst-order logic,the inductive data types,and type universes.Each of the components is described below.

Logic of LTT1The logical operators such as?,?and?are introduced by declaring as constants the operators and the direct proofs of the associated inference rules.For instance,for universal quanti?cation?,we declare(where we write‘f[a1,...,a n]’for applications and‘f[x1,...,x n]:A where x i:A i’for f:(x1:A1,...,x n:A n)A):

?[A,P]:P rop,?I[A,P,f]:P rf(?[A,P])and?E[A,P,a,p]:P rf(P[a]) where A:T ype,P[x:A]:P rop,f[x:A]:P rf(P[x])and p:P rf(?[A,P]).

Note that?can only quantify over types;that is,for a formula?[A,P], or?x:A,P[x]in the usual notation,A must be a type(of kind T ype).Since P rop is not a type(it is a kind),one cannot form a proposition by quantifying over P rop.Higher-order logical quanti?cations such as?X:P rop.X,as found in impredicative type theories,are not allowed.Similarly,since propositions are not types(P rf(P)is a kind,not a type),one cannot quantify over propositions, either.

As another example,we declare the classical negation operator?P:P rop for P:P rop and the corresponding double negation rule DN[P,p]:P rf(P) where P:P rop and p:P rf(??P)].Other logical operators can be introduced in a similar way or de?ned as usual.For instance,an equality operator can be introduced to form propositions a=A b,for A:T ype and a,b:A.

Inductive data types in LTT1The system LTT1(and every LTT)contains (some or all of)the inductive types as found in Martin-L¨o f’s type theory[NPS90] or UTT[Luo94],which include those of natural numbers,dependent pairs,lists, trees,ordinals,etc.For example,the type N:T ype of natural numbers can be introduced by?rst declaring its constructors0:N and s[n]:N where n:N, and then its elimination operator E T[C,c,f,n]:C[n],for C[n]:T ype with n:N, and the associated computation rules

E T[C,c,f,0]=c:C[0]

E T[C,c,f,s[n]]=f[n,E T[C,c,f,n]]:C[s[n]]

For each inductive type,there is an associated induction rule for proving properties of the objects of that type.For example,the induction rule for N is

E P[P,c,f,n]:P[n]for P[n]:P rop[n:N]

Note that the elimination operator over types,E T,has associated computational rules,while the elimination operator over propositions,E P,does not.

The induction rules are crucial in connecting the world of logical propositions (formally represented by P rop)and that of the data types(formally represented by T ype).Quanti?cations over types allow one to form propositions to express logical properties of data and the induction rules to prove those properties.

Type universes in LTT1The system LTT1(and every LTT)may contain type universes,types consisting of(names of)types as objects.For example,a universe of‘small types’can be introduced as

type:T ype and T[x]:T ype[x:type].

Some of the inductive types have names in a type universe.For example,we can have nat as a name of N in type by declaring nat:type and T[nat]=N:T ype. The general way of introducing type universes can be found in[ML84]and see, e.g.,[Luo94]for universes containing inductive types generated by schemata.

We remark that,if we have introduced a type universe that contains the names of N and?(the empty type),we can prove Peano’s fourth axiom for natural numbers(?x:N.(s[x]=N0))internally in the type-theoretic framework. This is similar to Martin-L¨o f’s type theory,where Peano’s fourth axiom is not provable internally without a type universe[Smi88].

Logical consistency of LTT1The system LTT1is logically consistent in the sense that there are unprovable propositions.If one is not satis?ed with the ‘simple minded consistency’[ML84],a meta-mathematical consistency can be proved–it can be shown that LTT1is relatively consistent w.r.t.ZF.

Theorem1(consistency).The type system LTT1is logically consistent.

Proof sketch Let T be Martin-L¨o f’s intensional type theory extended with Excluded Middle(i.e.,extending it with assumed proofs of A+(A→?)for all types A).Then T is logically consistent w.r.t.ZF.Now,consider the mapping :LTT1→T that maps the types and propositions of LTT1to types of T so that A =A for A:T ype and,e.g.,?[A,P] =Π[A ,P ]and(?P) =P →?. Then,by proving a more general lemma by induction,we can show that if Γ a:A in LTT1,thenΓ a :A in T.The logical consistency follows.

Although there are other ways to prove the meta-mathematical consistency, the above proof sketch raises an interesting question one may ask:if Martin-L¨o f’s type theory extended with a classical law(say Excluded Middle)is consistent, why does one prefer to use LTT1rather than such an extension directly?

One of the reasons for such a preference is that the LTT approach preserves the meaning-theoretic understanding of types as consisting of their canonical objects(e.g.,N consists of zero and the successors).Such an adequacy property would be destroyed by a direct extension of Martin-L¨o f’s type theory with a classical law,where every inductive type contains(in?nitely many)non-canonical objects.Therefore,in this sense,it is inadequate to introduce classical laws directly to Martin-L¨o f’s type theory or other type theories.

In our type-theoretic framework,there is a clear distinction between logical propositions and data types.For example,the classical law in LTT1does not a?ect the data types such as N.It hence provides an adequate treatment of classical reasoning on the one hand and a clean meaning-theoretic understanding of the inductive types on the other.

This clear separation between logical propositions and data types is an impor-tant salient feature of the type-theoretic framework in general.In Martin-L¨o f’s type theory,for example,types and propositions are identi?ed.The author has argued,for instance in the development of ECC/UTT[Luo94]as implemented in Lego/Plastic and the current version of Coq1,that it is unnatural to identify logi-cal propositions with data types and there should be a clear distinction between the two.This philosophical idea was behind the development of ECC/UTT, where data types are not propositions,although logical propositions are types.

Logic-enriched type theories,and hence our framework as presented in this paper,have gone one step further–there is a complete separation between propositions and types.Logical propositions and their totality P rop are not regarded as types.This has led to a more?exible treatment of logics in our framework.

2.2Implementation

The type-theoretic framework has been implemented by Callaghan by extending the proof assistant Plastic[CL01].Plastic implements the logical framework LF. The extension is to add the kind P rop and the operator P rf,as described at the beginning of this section.Logical operators such as those of LTT1are introduced by the user.Plastic already supports the inductive types in the kind T ype. However,it does not automatically generate the induction rules(represented above by E P for N)which,at the moment,are entered by the user(this is possible because E P does not have associated computation rules.)We should also mention that Plastic supports adding computation rules of certain form and this allows one to add universes and the associated computation rules.The system LTT1has been completely implemented in Plastic and so have the notions of set and the case studies to be described in the following two sections.

3Typed sets

When we consider sets in our type-theoretic framework,the objects of a set are all‘similar’in the sense that every set is a typed set.In other words,every set has a base type from which every element of the set comes.For instance,a set with N as base type contains only natural numbers as its elements.We believe that such a notion of typed set is natural and much closer to the practice of everyday mathematical reasoning than that in the traditional set theory where there is no distinction between types.Sometimes,mathematicians use the word‘category’for what we call types and consider sets with elements of the same category(see, e.g.,[Wey18]).Here,types are formal representations of categories.

In the following,we consider two notions of(typed)set:an impredicative notion and a predicative notion.

1The current type structure of Coq(version8.0)[Coq04],after the universe Set be-comes predicative,is very similar to(if not exactly the same as)that of ECC/UTT.

Impredicative notion of set Impredicative sets can be introduced as follows.–Set[A:T ype]:T ype(Set[A]is the type of sets with base type A.)

–set[A:T ype,P[x:A]:P rop]:Set[A](Informally,set[A,P]is{x:A|P[x]}.)–in[A:T ype,a:A,S:Set[A]]:P rop(Informally,in[A,a,S]is a∈S.)

–in[A,a,set[A,P]]=P[a]:P rop(Computational equality)

Note that this notion of set is impredicative.For example,the powerset of S: Set[A]can be de?ned as{S :Set[A]|?x:A.x∈S ?x∈S}of type Set[Set[A]]. Predicative notion of set The notion of predicativity has been studied by many people,most notably by Feferman in a series of papers,including[Fef05]. Intuitively,the de?nition of a set{x|p(x)}is predicative if the predicate p(x) does not involve any quanti?cation over the totality that contains the entity being de?ned.If the set-forming predicate p does not involve any quanti?cation over sets at all,then the de?nition of the set is predicative.

In our type-theoretic framework,predicative sets can be introduced by?rst introducing a propositional universe of small propositions:

prop:P rop,V[p:prop]:P rop

Intuitively,a small proposition contains only quanti?cations over small types (with names in type).This can be seen from the quanti?er rules for prop:

ˉ?[a,p]:prop[a:type,p[x:T[a]]:prop]

V[ˉ?[a,p]]=?[T[a],[x:T[a]]V[p[x]]]:P rop

where p[x]must be a small proposition for any object x in the small type a.

Formally,predicative sets can be introduced as follows:

–Set[a:type]:T ype(Set[a]is a type if a is a small type in universe type.)

–set[a:type,p[x:T[a]]:prop]:Set[a](Informally,p in{x:A|p[x]}must be a small propositional function.)

–in[a:type,x:T[a],S:Set[a]]:prop(Informally,x∈S is a small proposition.)–in[a,x,set[a,p]]=p[x]:prop(Computational equality)

Note that a type of sets is not a small type.Therefore,quanti?cation over sets is not allowed when stating a set-forming condition.

Remark1.Aczel and Gambino[AG02,GA06]have considered a type universe P of small propositions in the world of types(formally,P:T ype).Such a universe has played an important role in their study of the type-theoretic interpretation of constructive set theory.However,it seems that this has the e?ect of putting logical propositions directly‘back’to the world of types.In our case,the propo-sitional universe prop is of kind P rop,not of kind T ype.

We argue that the notions of set introduced above are adequate in support-ing‘mathematical pluralism’.2With these notions,the type-theoretic framework can be used to formalise,in the classical setting,the ordinary(classical and impredicative)mathematics and Weyl’s predicative mathematics and,in the in-tuitionistic setting,the predicative and impredicative constructive mathematics. 2The philosophical view of mathematical pluralism is to be elaborated elsewhere.

4Case studies

Formalisation of Weyl’s predicative mathematics As is known,the or-dinary mathematics is impredicative in the sense that it allows impredicative de?nitions that some people might regard as‘circular’and hence problematic. Such people would believe that the so-called predicative mathematics is safer, where impredicative or circular de?nitions are regarded as illegal.For instance, in the early quarter of the last century,the mathematician Hermann Weyl has developed a predicative treatment of the calculus(in classical logic)[Wey18], which has been studied and further developed by Feferman and others[Fef05].

The formalisation of Weyl’s work[Wey18]has been done in the type-theoretic framework(more speci?cally,in LTT1with predicative sets)in Plastic[AL06]. Formalisation and analysis of security protocols Security protocols have been extensively studied in the last two to three decades.Besides other interest-ing research,theorem provers have been used to formalise security protocols and prove their properties.For instance,Paulson has studied the‘inductive approach’[Pau98]in Isabelle[Pau94]to verify properties of security protocols.

As a case study of classical impredicative reasoning in the type-theoretic framework,we have formalised in Plastic several security protocols in LTT1 with impredicative sets.The examples include simple protocols such as the Needham-Schroeder public-key protocol[NS78,Low96]and the Yahalom protocol [BAN89,Pau99].Our formalisation has followed Paulson’s inductive approach closely,in order to examine how well the power of inductive reasoning in the type-theoretic framework matches that in Isabelle.Our experience shows that the answer is positive,although more automation in some cases would be de-sirable.In our formalisation,agents,messages and events are all modelled as inductive types(rather than as inductive sets as in Isabelle).The operations such as parts,analz and synth are de?ned as maps between sets of messages.A protocol is then modelled as a set of traces(a set of lists of events).One can then show that various properties are satis?ed by the protocol concerned,including the secrecy properties such as the session key secrecy theorem.

5Concluding remarks on future work

Future work includes comparative studies with other existing logical systems and the associated theorem proving technology.For example,it would be interesting to compare the predicative notion of set with that studied by Feferman and others[Fef00,Sim99]and to consider a comparison with that of Martin-L¨o f’s type theory[NPS90,ML84]to study the relationship between the notion of predicative set and that of predicative type.

Acknowledgements Thanks go to Peter Aczel for his comments during his visit to Royal Holloway,Robin Adams for discussions during our joint work on formalisation of Weyl’s predicative mathematics and Paul Callaghan for his e?orts in extending Plastic to implement the type-theoretic framework.

References

[AG02]P.Aczel and N.Gambino.Collection principles in dependent type theory.

Proofs and Programs,(eds)P.Callaghan,Z.Luo,J.McKinna and R.Pollack.

LNCS2277,2002.

[Agd00]Agda proof assistant.http://www.cs.chalmers.se/~catarina/agda,2000. [AL06]R.Adams and Z.Luo.Weyl’s predicative classical mathematics as a logic-enriched type theory.Submitted to TYPES’06,to appear,2006.

[BAN89]M.Burrows,M.Abadi,and R.Needham.A logic of authentication.Proc.

of the Royal Society of London,426:233–271,1989.

[C+86]R.Constable et al.Implementing Mathematics with the NuPRL Proof Devel-opment System.Pretice-Hall,1986.

[CH88]Th.Coquand and G.Huet.The calculus of https://www.sodocs.net/doc/0416847490.html,rmation and Computation,76(2/3),1988.

[CL01]P.C.Callaghan and Z.Luo.An implementation of typed LF with coercive subtyping and universes.J.of Automated Reasoning,27(1):3–27,2001. [Coq04]The Coq Development Team.The Coq Proof Assistant Reference Manual (Version8.0),INRIA,2004.

[Fef00]S.Feferman.The signi?cance of Hermann Weyl’s Das Kontinuum.Proof Theory,(eds)V.Hendricks et al.,2000.

[Fef05]S.Feferman.Predicativity.In S.Shapiro,editor,The Oxford Handbook of Philosophy of Mathematics and Logic.Oxford Univ Press,2005.

[GA06]N.Gambino and P.Aczel.The generalised type-theoretic interpretation of constructive set theory.J.of Symbolic Logic,71(1):67–103,2006.

[Gon05]G.Gonthier.A computer checked proof of the four colour theorem,2005. [HHP93]R.Harper,F.Honsell,and G.Plotkin.A framework for de?ning logics.

Journal of the Association for Computing Machinery,40(1):143–184,1993. [Low96]G.Lowe.Breaking and?xing the Needham-Schroeder public-key protocol using CSP and FDR.Lecture Notes in Computer Science,1055,1996.

[LP92]Z.Luo and R.Pollack.LEGO Proof Development System:User’s Manual.

LFCS Report ECS-LFCS-92-211,Dept of Computer Science,Univ of Edin-

burgh,1992.

[Luo94]https://www.sodocs.net/doc/0416847490.html,putation and Reasoning:A Type Theory for Computer Science.

Oxford University Press,1994.

[Luo03]Z.Luo.PAL+:a lambda-free logical framework.Journal of Functional Pro-gramming,13(2):317–338,2003.

[ML84]P.Martin-L¨o f.Intuitionistic Type Theory.Bibliopolis,1984.

[MN94]L.Magnusson and B.Nordstr¨o m.The ALF proof editor and its proof engine.

LNCS806,1994.

[NPS90] B.Nordstr¨o m,K.Petersson,and J.Smith.Programming in Martin-L¨o f’s Type Theory:An Introduction.Oxford University Press,1990.

[NS78]R.Needham and https://www.sodocs.net/doc/0416847490.html,ing encryption for authentication in large networks of https://www.sodocs.net/doc/0416847490.html,m.of the ACM,21(12):993–999,1978.

[Pau94]L.Paulson.Isabelle:a generic theorem prover.LNCS,828,1994.

[Pau98]L.Paulson.The inductive approach to verifying cryptographic protocols.

Journal of Computer Security,6:85–128,1998.

[Pau99]L.Paulson.Proving security protocols correct.LICS,1999.

[Sim99]S.Simpson.Subsystems of Second-Order Arithmetic.Springer-Verlag,1999. [Smi88]J.Smith.The independence of Peano’s fourth axiom from Martin-L¨o f’s type theory without universes.Journal of Symbolic Logic,53(3),1988.

[Wey18]H.Weyl.The Continuum:a critical examination of the foundation of analysis.

Dover Publ.1994,(English translation of Das Kontinuum,1918).

网页设计库和模板的应用

52门户网站实训指导（一） 实训目标： 1 掌握门户网站的设计技巧。 2 掌握库项目和模板的制作及使用方法。 实训步骤： 一创建站点。 在Dreamweaver CS3中定义一个本地站点，命名为“52menhu”，存储位置为：D：\sample\52menhu\，并将本项目素材文件夹下的图像文件夹image复制到网站的根文件夹下。然后，选择“窗口”→“资源”命令或者按F11键，打开“资源”面板。如图1。 图1 资源面板图2 新建库项目 二创建库文件。 单击“资源”面板右下角的按钮，新建一个库，然后在列表框中输入库的名称banner并加以确认。使用同样的方法创建名称为foot

的库文件。 二、制作主页的Banner 基本步骤: 1.在“资源”面板中双击打开，找到库文件banner.lbi。 2.插入一个3行1列，宽为760像素的表格。 3.设置表格属性(具体步骤参照书讲解)。 4.插入图片，输入文本。 最终效果如图3所示: 图3 banner效果图 制作页脚 基本步骤： （1）在资源面板中打开库文件foot.lbi； （2）插入一个3行1列,宽为760像素的表格； （3）设置表格属性，参数如图4； 图4 表格属性 （4）输入文本，并保存文件。效果如图5所示。

图5 页脚效果图 ●四、库项目的应用 ●1.插入库文件 新建页面myindex.html，依据前面做的banner.lib和foot.lib 文件充实首页面myindex.html。打开“资源”面板，点击左下角的“插入”按钮，分别将两个库项目分别插入到页面对应位置。 2.编辑库项目 在资源面板中单击“编辑”按钮，可打开库项目进行编辑。编辑的方法同编辑普通页面一样。 任务2 制作女性频道子页 1、使用模板建立子页 操作步骤： （1）将素材中的首页复制到站点中。选择“文件”→“另存为模板”命令，将已有页面另存为模板，命名为moban1。 2、定义可编辑区域 操作步骤： （1）选择“插入”→“常用”命令，单击“可编辑区域”按钮或者选择“插入”→“模板对象”→“可编辑区域”命令，打开“新建可编辑区域”对话框。

韩国农产品贸易概况

韩国农产品贸易概况 韩国作为一个贸易量在全球排名第十三的贸易大国，其农产品贸易量一直很大。韩国的农业种植主要集中在水稻生产，其大米供给量已基本实现自给自足的程度。小麦、玉米和大豆是韩国进口的主要农产品，且进口数量不断增加，。2002年分别增加到、和t。畜产品的进口主要是牛肉和牛奶，2002年分别进口了万和t。近年来，谷物、水果、蔬菜、畜产品等几乎所有农产品的进口都有增加。出口产品包括玉米、牛肉、皮革、大豆、面粉和棉花，2000年出口总额达26亿美元。其它主要出口国为澳大利亚（小麦、牛羊肉、羊毛、糖）；马来西亚（橡胶、棕榈油）；新西兰（牛肉、猕猴桃、奶制品）；加拿大（谷物饲料、油菜籽）；欧盟（猪肉、谷物饲料、肉制品）和中国。中国自1984年开展对韩贸易以来，出口的产品越来越多，其中最主要的是谷物饲料，并在这个市场中具有一定的竞争力。 韩国农产品的出口不多。1997年农产品的出口，包括猪肉、苹果、泡菜、方便面、人参和人参制品，其价值不到进口农产品的20％和农业产值的5％。日本是韩国农产品的主要出口国，1997年对日出口占全部出口的37％（指农林产品，不包括水产品）。

韩国逐步开放大米市场 大米自给 韩国自70年代后期起就通过政府的大量干预实现了大米自给（个别欠收年份除外）。60和70年代水稻产量持续增长，直到80年代后期才开始逐渐下降。人均大米消费在80年代以前一直在不断上升，但自87年起几乎年年下降。 70年代，韩国政府决定采取联合措施来推动实现水稻自给。这一措施包括两项内容，即提高水稻产量和限制水稻消费。首先是引进高产的统一稻（Tongil）和杂交稻（印度稻与日本稻的杂交品种），尤其是统一稻产量更高，稻农纷纷转向这个新品种；同时，提高国内大米收购价，使稻农收入增加。然而1980年6月的一场寒流摧毁了统一稻的收成，极大地挫伤了农民对新品种的信心，并造成大米市场供应的严重短缺。政府只好紧急进口100多万吨大米。随后，农民陆续改种日本稻，该品种虽然产量低，但抗寒能力较强。 与此同时，政府通过各种手段干预大米消费市场。首先是对水稻进口实行国家垄断，通过禁止水稻进口（除1980年的特殊情况外）来提高国内大米零售价。其次，政府下令在食品制作中将大麦、小麦与大米混合使用以减少大米的用量。绝大部分水稻加工被禁止。因消费者不喜欢统一稻的味道，政府便通过提高收购价格来引诱农民继续种植统一稻，尤其是在发生了1980年自然灾害以后，仅 1986-1988两年收购价就提高了116%。同时以较低价来引诱消费者购买。由于政府在稻米生产上的政府预算赤字急剧膨胀，政府不得不考虑通过扩大征税来对农民进行补贴。 1991年政府停止收购统一稻。由于没有其它销路，统一稻种植终止了。尽管大米人均消费量持续下降，但由于产量下降，韩国大米储备在94-96年期间降至历史最低水平。劳动力价格的提高使大米种植业失去了对众多小型农场的吸引力。水稻种植面积逐年递减。 大米进口 当前韩国政府的大米进口政策是"不求质优，只求价廉"，这使国外优质的日本大米很难进入韩国大米市场主流。韩国原本是全球对大米质量要求最高的，但现在消费者却要为国产大米支付高于国外优质大米的价格。因此，这个市场对于加利福尼亚、澳大利亚和中国北方等大米主要出口地区极具诱惑。加入WTO后，韩国同意从1995年开始最低限度地放开大米进口。195年，韩国按照最低报价进口了印度大米，随后几年，又以同样方式从中国进口了大米。借助进口，韩国的大米储备在1997年后迅速恢复。但由于消费量减少的态势仍在加剧，大米储备急剧增加，因此，韩国"大米市场管理委员会"建议将收购价降低4 -5%，但遭到农业生产部门的强烈反对，最终政府宣布2002年的水稻收购价保持不变。 关于乌拉圭谈判的减让承诺 同其它WTO签字国一样，韩国承诺根据1995乌拉圭协议进行政策调整。总体上讲，该协议带来了市场准入方面的改善（降低关税、增加配额、取消进口禁令），限制了出口补贴和产生扭曲贸易的国内支持，并增加了对假借进出口卫生检疫措施构筑贸易壁垒现象的追索权。韩国向WTO通报不实行农业出口补贴。在动植物检疫方面，韩国同意一切与卫生检疫相关的限制进口措施必须有科学证据。韩国还在市场准入和综合支持量方面做出了具体承诺。 大米进口是韩国国内广泛关注的问题。事实上，近几十年来大米进口基本上是被禁止的。在乌拉圭谈判中，韩国同意逐渐增加最低市场准入量。根据乌拉圭协议的要求，韩国

原产地证 附样本

原产地证 C/O为CERTIFICATE OF ORIGIN的简称，意思为“原产地证书”，以下为具体内容。 一、原产地证书的作用 原产地证明书（CERTIFICATE OF ORIGIN）是出口商应进口商要求而提供的、由公证机构或政府或出口商出具的证明货物原产地或制造地的一种证明文件。原产地证书是贸易关系人交接货物、结算货款、索赔理赔、进口国通关验收、征收关税在有效凭证，它还是出口国享受配额待遇、进口国对不同出口国实行不同贸易政策的凭证。 二、原产地证书的类型 根据签发者不同，原产地证书一般可分为以下三类： ①商检机构出具的原产地证书， 如：中华人民共和国检验检疫局（CIQ）出具的普惠制产地证格式A（GSP FORM A）；一般原产地证书（CERTIFICATE OF ORIGIN）。 ②商会出具的产地证书， 如：中国国际贸易促进委员会（CCPIT）出具的一般原产地证书，简称贸促会产地证书（CCPIT CEERTIFICATE OF ORIGIN）； ③制造商或出口商出具的产地证书； 在国际贸易实务中，应该提供哪种产地证明书，主要依据合同或信用证的要求。一般对于实行普惠制国家出口货物，都要求出具普惠制产地证明书。如果信用证并未明确规定产地证书的出具者，那么银行应该接受任何一种产地证明书。现在我国多数出口商习惯于使用贸促会出具的证书。 三、原产地证书的申请 根据我国的规定，企业最迟于货物报关出运前三天向签证机构申请办理原产地证书，并严格按照签证机构的要求，真实、完整、正确地填写以下材料： ①《中华人民共和国出口货物原产地证书/加工装配证明书申请书》； （见附页）此处显示一份《一般原产地证明书/加工装配证明书》图5-1（国际商务单证103） ②《中华人民共和国出口货物原产地证明书》一式四份； ③出口货物商业发票；

韩国SM公司_造星模式

韩国SM公司造星模式（转） 在韩国有“星工厂”之称的SM公司老总李秀满20世纪70年代初涉歌坛，是当时非常著名的歌手。退居幕后之后，凭借其敏锐的眼光，于1989年创办了SM娱乐文化公司，开创了韩国企划公司的新时代。1998年，.公司把旗下的HOT、SES介绍到中国、日本，掀起了亚洲“韩流”热潮。2000年4月，.公司登记注册了KOSDAQ，发行股票，成为韩国第一个娱乐文化股份公司。2001年，.培养的宝儿又在日本跻身最受欢迎的歌手行列。2002年12月，.公司与日本的FANDANGO JAPAN（YOSHIMOTO集团和KDDI的合资公司）、YOSHIMOTO集团以及AVEX共同创立了网络娱乐公司---FANDANGO KOREA，在网络与移动通信迅速发展的时代，将主要负责为大众开发数字信息资源。今年为了方便进入中国市场，在中国设立了分公司，与2001年成立的.日本分公司一起，共同构建亚洲地区的娱乐网络。.公司不懈努力，把世界知名的美国时代华纳、迪斯尼等娱乐集团，作为自己未来的目标，希望成为亚洲地区最强的娱乐集团。 .公司下设部门：发觉“未来之星”的选秀部；训练新人的“Starligh t Academy”培训部；把握市场走向、体现歌手风格、营造逼真视觉感的唱片生产部；进行录音和后期制作的唱片制作部(A&R)；进行宣传销售的市场营销部；联系媒体对歌手进行推广的宣传部；以及发掘歌手的潜在价值、企划广告演唱会的代理部。其实韩国的娱乐公司不下数十家，其中包括JYP Entertainment、DSP Entertainment、Laful Entertainment、DR Music、Music Factory、Good Media和 Media等，之所以SM能在诸多强劲对手中独占鳌头，还是凭借公司领导层的独具慧眼和完整专业的运作体系，才创造出HOT、安七炫（KANGTA），神话，宝儿（BOA），文熙俊，， FlytotheSky，Trax，东方神起! ，天上智喜这些享誉亚洲歌坛的著名歌手。 第一步：选秀&培训（选秀部、培训部）

韩国大企业模式的功与过

韩国大企业模式（财阀或财团）的功与过韩国仅用了30年的时间，就迅速完成了工业化，创造了震惊世界的“江汉奇迹”，成为世界“经济大国”和“贸易大国”，被誉为“亚洲四小龙”之一和“发展中国家经济复兴的样板”。韩国经济得以高速发展和迅速成功的原因固然是多方面的，但其中关键的因素就是其大企业财阀在经济发展和工业化中发挥了堪称中流砥柱的作用。 韩国学者林炳润曾指出:“财团就是韩国经济之全部的比喻，并非夸大其辞。由于财团在整个国民经济中所占的比重和发挥的作用如此巨大，故可以说，没有对财团的理解，就不能理解韩国的经济。”[1]然而，同样令世界震惊的是，在1997年亚洲金融风暴的席卷下，一批过去被称为韩国经济支柱或中坚的大企业集团纷纷倒闭、破产或陷入经营危机中，使韩国经济遭受重创。近来发生的几件事更让世界震惊不已:“大宇帝国”的雪崩、“三星集团”的重组和“现代王国”郑氏父子的淡出，似乎都在预示着韩国的大企业发展模式已经走到尽头。本文在此对韩国大企业发展模式的利弊得失作一探讨，以求教于学术界同仁。 一、韩国大企业发展模式的缘起 韩国财阀及大企业发展模式，是以日本殖民统治时期的民族工商业为起点逐步形成和发展起来的。

1．萌芽期（30年代—40年代中期）。当时韩国一批年轻人利用日本扩大侵华战争和发动太平洋战争所带来的“军需景气”和日本财阀向朝鲜半岛转移部分产业的有利时机，开始涉足实业界，在日本殖民统治的夹缝中从事商业和服务业。他们通过掠夺土地和从事大商业经营，完成了资本原始积累，逐步扩大经营范围，从而建立起大的企业集团，如“三养”、“和信”和“开丰”等财阀。这批战前就形成的财阀规模较小，一般都以小型工商业为经营主体，直到50、60年代以后才发展成为垄断财阀，所以也被称为“原始型财阀”。 2．成长期（40年代末—50年代中期）。它们主要借助于韩国经济复兴的良机，依靠“归属财产”、美国的经济援助和政府的“特惠扶持”发展起来的。1947年，美国占领当局将没收日本殖民所有（包括2575家企业、库存物品、不动产及相当于朝鲜半岛15％的土地，相当于韩国总资产的80％）的所谓“归属财产”，经李承晚政府之手几乎无偿地“处理”给私人企业。1945－1961年，美国向韩国提供了大约21.5亿美元的物质援助。韩国政府将其出售所得占当时财政收入的40％左右，以此充当对工商业贷款和投资的来源。[2]那些与政府有密切关系的官商利用这一机会，通过购买归属财产、外国援助分配和政府在金融等方面给予特惠等途径发展，形成一批特权财阀，如“三星”、“乐喜金星”、“大韩”、“东洋”等，因此而被称为“特惠财阀”。

原产地证明书样本(完整版)

原产地证明书样本 原产地证明书样本。 sampleertifiateoforigin asia-paifitradeagreement 1.goodsonsignedfrom: refereneno. issuedin……………. goodsonsignedto: 3.foroffiialuse 4.meansoftransportandroute: 5.tariffitemnumber: 6.marksandnumberofpakages: 7.number andkindofpakages desription ofgoods: 8.origin riterion 9.gross eight orother quantit:

10.numberanddateofinvoies: 1 1.delarationbtheexporter: theundersignedherebdelaresthattheabovedetailsandstatement sareorret:thatallthegoodsereproduedin ………………………………. andthatthepliththeoriginrequirementsspeifiedforthesegoods intheasia-paifitradeagreementforgoodsexportedto ………………………………. ………………………………. plaeanddate,signatureofauthorized signator1 ertifiate itisherebertifiedonthebasisofontrolarriedout,thatthedelar ationbtheexporterisorret. ………………………………… plaeanddate,signatureandstampof ertifingauthorit notesforpletingertifiateoforigin i.generalonditions: toqualifforpreferene,produtsmust: a)fallithinadesriptionofprodutseligibleforprefereneinthel istofonessionsofanasia-paifitradeagreementountrofdestination;

7-1 第七章 问卷设计(习题)

第七章问卷设计 一，辨析题 1，电话访问常用语过滤样本或作简短的调查 2，尽量使用私人信函而非公函，尽量粘贴有价值的邮票而不采用加盖的邮资已付戳等都可以增加邮寄访问问卷的回收。 3，一般来说，人员面对面访谈的问卷设计要周密、明确一点，而邮寄调查问卷可以相对灵活点。 4，双重问题是指问题表述模糊不清。 二、名词解释 1.问卷 2.问卷设计 3.封闭式问题 4.开放式问题 5.假设性问题 6.作业证明记载 三、单选题 1.一般来说，邮寄访问问卷在寄出( )天内回收比较适当

A．5-10天 B.10-15天 C．15-20天 D.20天以上 2.电话访问问卷最主要的特点是（） A.成本较低 B.便于操作 C.简洁明了 D.回收率高 3.邮寄访问问卷最大的缺陷是（） A.成本较高 B.操作较难 C.设计较难 D.回收率低 4.现在你用何种牌子洗衣粉？这是（） A.事实性问题 B.动机性问题 C.态度性问题 D.假设性问题 5.（）是调查者在提出问题的同时，还将问题的一切可能答案或几种主要可能答案全部列出，由被调查者从中选出一个或多个答案作为自己的回答，而不做答案以为的回答。 A.指导性问题 B.动机性问题 C.开放性问题 D.实质性问题 6.（）为收集个人意见的理由或行为的动机等资料而设

计的问题。 A.事实性问题 B.动机性问题 C.态度性问题 D.假设性问题 7.“XX”啤酒制作精良，泡沫丰富，味道纯正，您是否喜欢？防了（）方面的错误。 A.不易回答 B.容易引起误解 C.使用了不恰当的假设 D.诱导性问题 8.（）问卷的说明词最简单。 A.电话访问 B.邮寄访问 C.小组讨论 D.面对面访问 9.问卷设计必须遵循一个符合逻辑的循序，经过长期的实践总结，人们总结出基本的步骤，其中问卷设计的第一步是（） A.明确调查对象的类型和特点 B.明确调研主题与所需的资料 C.明确数据收集的方法 D.设计问卷 10.调研问句可分为不同的类型，当问句是“你为什么购买

中国应该学习韩国模式 (1)

中国应该学习韩国模式 2012-2-28 每日经济新闻一些依靠低端制造、低成本、污染环境、大规模扩张迅速发展的企业，正成为实业界的裸泳者。 全球造船业进入寒冬期，中国是寒冬期的北极。 从数量上看，中国造船业在跨越式发展。2011年，在全球造船业不景气的背景下，中国在新接订单量、手持订单量和建造量这三大指标上超越韩国成为世界第一。2011年下半年，已有一些造船企业倒闭，数据不错是因为恰逢上一轮订单交货期。 中低端造船市场面临大整合，中船集团公司总经理谭作钧预计我国造船企业将有一半消失。迹象如此明显，接到的订单接近于零，今年1月，中国造船厂获得9艘船订单，共计11.22万修正总吨（CGT），全球市场占有率为22.4%，同比锐减了78%，多数船厂订单为零。根据中国船舶工业行业协会最新披露的数据，2011年全国船厂新承接船舶订单量3622万载重吨，同比下降51.9%，约有1/3企业没有接到订单。今明两年，世界船舶工业面临的发展环境将更加严峻。预测2012年世界新船订造量约为7000～8000万载重吨，造船完工量约1.5亿载重吨左右。船舶供需失衡，新船价格将可能继续下滑。 更糟的是，造船行业亏本赚吆喝。浙江台州枫叶造船厂的负责人表示，“现在造一艘船，基本不赚钱，甚至亏本，大家都在接单养工人，熬着。”以在造的3万吨散货轮为例，2008年上半年一艘可以卖到3亿多元，2009年降到2.4亿元，去年底报价1.7亿元，现在可能只值1.6亿元。3年多时间，船舶销售价降了一半多，但钢材、人工的成本却一直在涨。 韩国造船业也面临延期交货要求等困境，但总体而言日子还能过得下去。接单数量上升，去年1月至9月，在全球船舶订单量较去年同期减少22.3%的情况下，韩国企业的接单总量反而同比增加17.2%，达到1207万修正总吨，占全球订单总量的51.2%。 去年开始全球造船行业急剧分野，高的越高，低的越低：有技术、有创新能力的吃盛宴，没有技术能力的连残羹都无。2011年全球新船订单数量同比下降50%左右，但订单总金额仍达到900亿美元，同步仅下跌10%，高附加值船舶的订单量没有减少反而在增加。 技术优势成为支撑韩国造船业度过寒冬的法宝。2011年在经济紧缩的逼迫之下，全球造船业需求结构发生突变，此前是春风之下的共同发展，有技术的卖技术，没技术的卖力气，现在则变成不得不订货的高附加值船舶独占天下。国际船舶市场需求结构发生了重大变化，我国具有竞争优势、技术含量不高、用工集中的散货船、油船等需求量和价格急速下跌，而超大型集装箱船、液化天然气船（LNG）等高技术、高附加值船型在整个市场需求结构中所占比重显著提升。韩国造船业凭借技术、产品结构优势和政府金融支持等手段，承接了超大型集装箱船、LNG船和大型海洋工程装备的大部分订单。 面向未来，除了技术壁垒之外，中国船舶企业还得增加环保意识，耗油量低的低碳模式将是未来船东的必然要求。 韩国造船行业是其他行业的缩影，在本轮金融危机中，韩国经济堪称奇迹，在全球经济萧条之时，韩国、土耳其等国却异军突起，尤其是韩国在高技术领域对日本的替代作用令人刮目相看。 韩国的成功首先得益于国际化。2月18日，《经济学人》发表的文章标题就

韩国十大化妆品品牌

韩国十大化妆品品牌 1. 婵真- 绝对是韩国的一线品牌,是第一个打入日本化妆品市场的韩国品牌,要知道日本是化妆品的强国,不具备相当的实力,很难打入它的市场。因为婵真只生产护肤品,生产规模和产量并不大,但在韩国却有着“韩国女性化妆品第一品牌”的美誉。它是第一个获得在日本市场的销售许可的韩国化妆品牌。 2. 爱茉莉- 太平洋集团作为韩国排名第一、世界化妆品排名前二十名的国际化妆品集团,她无疑就是韩国女性的美丽秘密所在。集团旗下的第一大品牌laneige兰芝是目前韩国女性化妆品市场占有率最高的化妆品。全球亦排列前20位。而据专业人士所讲,laneige最适合少女至25岁左右的女士。 3. 生格林(Seang-green) - (株) 生格林公司于1987年创建，主要生产及供应优秀的韩方化妆品和保健食品及医药外品的公司，由于其以中药方的纯植物性药材的优秀效能与实体科学有机结合，使韩国消费者体会到自然配方的优秀功效和安全性，使其在十几年的时间一举跃上韩国化妆品的第三大位置。目前生格林的产品在韩国、台湾、新加坡等亚太地区都有很大的销量和消费群。它以无色、无味、无毒的纯自然性中草药成分为原料，在去斑美白、抗皱防老的功能性产品上更是具有独一无二的专利权，在韩国市场尤其在演艺界有非常高的知名度和口碑。 4.爱之浓丝ISA KNOX - 是进口蝶妆中的极品品牌。以满足

女性追求滋润有光泽的皮肤为基础,强化细胞结合水,采用Ceramide液晶乳化技术、三重保湿效果、科学认证地效能效果,开发出专门性的高保湿化妆品。 5. 三星迪奥普雷斯化妆品(DEOPROCE)：deoproce是三星samsung下面的一个牌子deoproce,这个牌子的标志是一朵玫瑰,具优异的卸妆效果,丰富的维他命成份及天然植物精华供给肌肤所必需的酸素,延缓皮肤老化,从而使皮肤变的更加洁净、滑嫩。丰富细腻的泡沫能温和清洁肌肤,有效清除面部多余的油脂及污物。独有细致的洁面柔珠,彻底清洁老化角质及毛孔内的污垢,保持肌肤一整天的干爽,令皮肤倍感爽洁、清透。有消炎,镇静肌肤的作用。 6.爱丽化妆品(ETUDE)：拥有ETUDE爱丽两用粉饼、ETUDE爱丽光彩细致隔离霜~绿、ETUDE爱丽卸妆水、ETUDE 爱丽光彩细致粉底液、ETUDE爱丽光彩细致蜜粉饼、ETUDE 爱丽双子星睫毛膏等产品。产品追求谈雅自然。 7.多多化妆品(DODO)：韩国DODO化妆品股份有限公司于1994年开始进入大众消费市场。截至到现在全国拥有40多家百货公司专柜及140多家特约经销商店,且不断地推出新产品。在化妆品市场日渐成熟的北京,又一家大型跨国企业———多多化妆品股份有限公司6月11日落户京城,其产品正式登陆中国市场。DODO现在是韩国最大的彩妆公司,生产的彩妆非常有名气,“演员粉”又叫“红色恋人”是该品牌中最有名气的产品之一了。是

产地证模板2

ORIGINAL 1.Products consigned from(Exporter's business name, address, country) 发货方 发货企业英文名称（必须和备案的一样） 发货企业英文地址（必须有CHINA） Reference No. 2.Products consignee to (Consignee’s name，address，country) 收货方 收货企业英文名称 收货企业英文地址（必须有收货国家英文） 3.Means of transport and route(as far as known) 运输方式日期…...…………………………………………Departure Date : 开船日期 Vessel /Flight/Train/Vehicle No.船名航次 Port of discharge : 目的港 运输路线描述(如：FROM SHANGHAI CHINA TO NEW YORK USA BY SEA) Item number 1 2 3 6.Marks and number of packages 唛头 N/M 7.Number and kind of packages，description of goods 品名和包装数量 货物英文描述 货物HS编码 货物英文描述 货物HS编码 货物英文描述 货物HS编码 具体包装及数量： （如：10CTNS,10PLTS,10CASES等等） **** **** **** **** 8.Origincriterion(see Notes overleaf) 9.Gross weight or other quantity and value(FOB) 数量/金额 货物数量及单位 货物FOB美元金额 货物数量及单位 货物FOB美元金额 货物数量及单位 货物FOB美元金额 10.Number and date of invoices 发票号及日期 发票号码： 发票日期： C11.Declaration by the exporter he undersigned hereby declares that the above detail and statements are correct that the goods were produce in -------------------------------------------------------------------------- 我司盖印 -------------------------------------------------------------------------- Place and date, signature of authorized signatory CHECK MARK ON THIRD PARTY INVOICING 12.Certification It is hereby certified，on the basis of control carried out, the Declaration by the exporter is correct. 商检局盖印 ---------------------------------------------------------------------------- Place and date. signature and stamp of certifying authority

韩国文创融资模式

韓國文創產業融資發展模式之借鑒 侍安宇1梁連文2黃博怡3 摘 要 近年來韓流快速席捲亞洲國家，反映韓國過去長期累積的各類文化及創意實力，蛻變創造了文化經濟的蓬勃發展。在金融協助方面，從韓國的運作經驗了解，韓國政策的優點在於政府之政策主導性強，且對信用保證、評價(等)機構與政策性專業銀行掌握絕對之控制權。換言之，在政府強勢主導之下，韓國文創產業投融資兼顧了評價(等)、信用保證及金融機構等各方面。不過，韓國經驗雖有許多值得台灣借鏡之處，但因國情及基礎金融環境不同，且其政府主導力度強，故不必然我國均可適用。本文擬藉由介紹及分析韓國文創產業融資之發展模式及配套措施，提出對我國在文創產業投融資之建議。 關鍵詞：文創融資、KOTEC、Kibo、KTRS、評價(等)、完工保證 壹、前言 文化創意產業並非無中生有，它奠基於一個國家長時間所累積的各項實力，包含歷史、文化、工藝、科技、商業等。經過融合深化之後，它可以成為知識經濟時代促進經濟發展暨產業升級的重要力量。換言之，文化創意產業反映一個國家的文化底 1台灣金融研訓院金融研究所副研究員。 2中國文化大學財務金融系副教授。 3實踐大學財務金融學系教授兼管理學院院長。 85

蘊，文化底蘊深厚的國家，配合適當的技術與制度，便有機會孕育發展出豐富多樣且具市場價值的文創產業。近年快速席捲亞洲國家，並迅速擴展到美洲和拉丁美洲國家，甚至在歐洲、澳洲及非洲也逐步抬頭的韓流(Hallyu)，即明顯反映韓國過去長期累積的各類實力，蛻變出多元色彩，創造了文化經濟。韓國戲劇、電影、音樂、料理及韓語的流行，使韓國成為世界十大文化產品輸出國之一，並隨著三星、LG、現代等大型跨國公司的發展，韓流已成為韓國經濟崛起的代名詞。 一直以來，韓國的中小企業政策及科技技術發展通常由政府強勢主導，通常是政府政策在先，企業配合政策積極開發各項技術。但有關韓流的相關產業，其發展正好相反。韓流可以說是由韓國人的個性好強或民族性而帶動出現的，當韓流發展一定程度之後，政府再因應推出相關政策，如文化體育觀光部(Ministry of Culture, Sports and Tourism，簡稱MOCST)成立文化產業振興院(Korea Creative Content Agency，簡稱KOCCA)，又與技術信用保證基金(Korea Technology Finance Corporation，簡稱KOTEC或Kibo)合作共同研發適用於文創產業之評等系統。 在保證及評價(等)方面，韓國透過成立KOTEC來針對高新技術及智慧財產等複雜且高風險產業提供保證及技術評價(等)，以利高新科技產業之資金融通與產業發展。2013年底其專業技術評估人員已達578人，其中147人具有博士或同等學力。KOTEC初期對高新科技及文創產業並不甚瞭解，花了將近10年時間瞭解這類產業，其間有很多失敗的經驗，但也因此累積很多直覺。經由KOTEC團隊討論出一些重要的評估項目，並與實務專家對評估項目進行討論，結合這些專業人員的意見及KOTEC之技術才逐步發展出適用於不同產業之技術評等系統(Kibo Technology Rating System，簡稱KTRS)。 86

韩国贸易现状分析

2005国别贸易投资环境报告--韩国 https://www.sodocs.net/doc/0416847490.html, 2005年04月01日 18:50 新浪财经 新浪财经讯中华人民共和国商务部公布2005国别贸易投资环境报告，以下为该报告韩国部分。 一、双边贸易投资概况 2004年，韩国是中国第五大贸易伙伴。据中国海关统计，2004年中韩双边贸易总额为900.7亿美元，同比增长42.5%。其中，中国对韩国出口278.2亿美元，同比增长38.4%；自韩国进口622.5亿美元，同比增长44.3%。中方逆差344.3 亿美元。中国对韩国出口的主要产品为服装及衣着附件、纺织纱线、织物及制品、化工产品、钢铁及其制品、玉米、煤、铝及其制品、电视机零附件、收音机及无线电通讯设备的零附件、水产品、海产品、集成电路及微电子组件等；自韩国进口的主要产品为集成电路及微电子组件、钢铁及其制品、塑料及其制品、移动电话机、电视机零附件、收音机及无线电讯设备的零附件、消费类电子产品及零件、有机化学品、自动数据处理设备的零件、铜及其制品、彩色图像显示管等。 据中国商务部统计，2004年，中国公司在韩国完成承包工程营业额1亿美元，新签合同金额1.7亿美元；完成劳务合作合同金额2.8亿美元，新签合同金额2.3亿美元。截至2004年底，中国公司在韩国累计完成承包工程营业额2.2亿美元，签订合同金额4.1亿美元；完成劳务合作合同金额20.5亿美元，签订合同金额25.7亿美元。 2004年，经中国商务部批准或备案，中国在韩国设立非金融类中资企业19家，中方协议投资额6.1亿美元。截至2004年底，中国在韩国累计投资设立非金融类中资企业91家，中方协议投资总额9.1亿美元。 据中国商务部统计，2004年，韩国对中国投资项目5625个，合同金额139.1亿美元，实际使用金额62.5亿美元。截至2004年底，韩国累计对中国直接投资项目32753个，合同金额505.6亿美元，实际使用金额为259.4亿美元。 二、贸易投资管理体制概述 (一)贸易投资管理法律体系 韩国涉及贸易投资管理的法律主要包括《对外贸易法》、《外国人投资促进法》、《关税法》、《外汇交易法》和《有关提高出口产品质量法》等。其中，《对外贸易法》和《外国人投资促进法》是韩国贸易和投资管理领域的基本法律。 此外，韩国产业资源部还通过定期或不定期公布《进出口公告》、《进出口统合公告》和《进出口特别公告》来确定进出口贸易的各项具体政策。

原产地证明样本

原产地证明样本 SAMPLE CERTIFICATE OF ORIGIN Asia-Pacific Trade Agreement (Combined declaration and certificate) consigned from: (Exporter’s businename, address, country) Reference No. Issued in ……………. (Country) 2. Goods consigned to: (Consignee’s name, address, country) Official use 4. Means of transport and route: item number:6. Marks and number of Packages: 7. Number and kind of packages/ description of goods: 8. Origin criterion (see notes overleaf)9. Gross

weight or other quantity:10. Number and date of invoices: 11. Declaration by the exporter : The undersigned hereby declares that the above details and statements are correct: that all the goods were produced in ………………………………. (Country) and that they comply with the origin requirements specified for these goods in the Asia-Pacific Trade Agreement for goods exported to ………………………………. (Importing Country) ………………………………. Place and date, signature of authorized Signatory 12. Certificate It is hereby certified on the basis of control carried out, that the declaration by the exporter is correct. ………………………………… Place and date, signature and Stamp of

关于韩国出口产品检查

关于韩国出口产品检查 1.洋葱汁、白菜汁、洋白菜汁、萝卜汁等检查基准 （1）食品公典分类：果蔬类饮料（小分类：果蔬汁） （2）食品公典果蔬类饮料规格 - 铅（mg/kg）：0.3以下 - 镉（mg/kg）：0.1以下 - 锡（mg/kg）：150以下（限在罐头产品） - 细菌总数：每克100,000以下 - 大肠菌群：阴性（限在加热产品） - 肠出血性总黄曲霉毒素大肠杆菌：阴性（非加热产品） - 防腐剂：苯甲酸0.6g/kg，paraoxybenzoic acid 0.1g/kg以下 （3）食品公典共同规格 - 三聚氰胺：2.5mg/kg以下 （4）2011年对最初进口食品精密检查的重点检查项目 铅、镉、锡（罐头产品）、细菌总数、肠出血性大肠杆菌(非加热产品)、防腐剂→洋葱汁、白菜汁、洋白菜汁、萝卜汁韩国法定检查基准是 铅、镉、细菌总数、大肠菌群、防腐剂、三聚氰胺 2.香菇汁、虾汁、香菇调味粉检查基准 （1）食品公典分类：规格外一般加工食品 （2）食品公典规格外一般加工食品规格 - 性状：适合 - 异物：适合 - 酸价：食用油脂加工品3.0以下，芝麻粉及大豆粉：4.0以下 食用蚕蛹加工品及油炸·油处理制品：5.0以下 - 过氧化值：60以下（限在食用蚕蛹加工品或油炸·油处理制品） - 重金属（mg/kg）：10以下（限在食用油脂加工品或糖类加工品） - 大肠菌群：阴性（限在杀菌制品） - 细菌总数：阴性（限在灭菌制品） - Tar色素、防腐剂、抗氧化剂是根据添加剂公典中规定的使用基准检测，根据重要性选择性适用。

（3）食品公典共同规格 - 三聚氰胺：2.5mg/kg以下 （4）2011年对最初进口食品精密检查的重点检查项目 大肠菌群（杀菌制品）、细菌总数（灭菌制品）、Tar色素、合成防腐剂、 抗氧化剂、酸价（芝麻粉、大豆粉、食用蚕蛹、加工品、油炸·油处理制品）→香菇汁、虾汁、香菇调味粉的韩国法定检查基准是 香菇汁：性状，异物，三聚氰胺 虾汁：性状，异物，三聚氰胺，（Nitrofuran） 香菇调味粉：性状，异物，三聚氰胺，（辐照） 3.大蒜汁、蔬菜包检查基准 （1）食品公典分类：果蔬加工品类（小分类：果蔬加工品） （2）食品公典果蔬加工品规格 - 大肠杆菌：阴性 - Tar色素：不得检出 （3）食品公典共同规格 - 辐照：辐照时标示 - 三聚氰胺：2.5mg/kg以下 （4）2011年对最初进口食品精密检查的重点检查项目 - Tar色素，大肠杆菌 →大蒜汁、蔬菜包的韩国法定检查基准是 大蒜汁：Tar色素，大肠杆菌，三聚氰胺 蔬菜包：Tar色素，大肠杆菌，三聚氰胺，辐照（蔬菜包） 4. 辣椒调味油、洋葱调味油检查基准 （1）食品公典分类：食用油脂类（小分类：香味油） （2）食品公典香味油规格 - 酸价：3.0以下 - Tar色素：不得检出 （3）食品公典共同规格 - Benzo(a)pyrene：2ug/kg以下 - 三聚氰胺：2.5mg/kg以下 （4）2011年对最初进口食品精密检查的重点检查项目

原产地证明书样本模板(精选多篇)

原产地证明书样本(精选多篇) 第一篇：原产地证明书样本 原产地证明书样本 原产地证书是证明货物的生产或制造地的文件，简称原产地证，原产地证书在国际贸易中往往被进口国用来作为实行区别关税待遇和实施国别贸易政策管理的重要依据，例如最惠国待遇、政府采购、保障措施的正确实施等等，因此具有待定的法律效力和经济作用。下面是亚太贸易协定的原产地证明书，供大家参考。 samplecertificateoforigin asia-pacifictradeagreement (combineddeclarationandcertificate) 1.goodsconsignedfrom: (exporter’sbusinename,address,country) referenceno. issuedin……………. (country) 2.goodsconsignedto: (consignee’sname,address,country) 3.forofficialuse 4.meansoftransportandroute:

5.tariffitemnumber: 6.marksandnumberofpackages: 7.number andkindofpackages/ description ofgoods: 8.origin criterion (seenotes overleaf)9.gross weight orother quantity:10.numberanddateofinvoices: 11.declaratio(本文来自)nbytheexporter: theundersignedherebydeclaresthattheabovedetailsandstateme ntsarecorrect:thatallthegoodswereproducedin ………………………………. (country) andthattheycomplywiththeoriginrequirementsspecifiedforthe segoodsintheasia-pacifictradeagreementforgoodsexportedto ………………………………. (importingcountry)

电子竞技商业模式比较——欧美模式VS韩国模式

电子竞技商业模式比较——欧美模式VS韩国模 式 目前，在全球范围内，电子竞技产业发展得比较好的的是美国、欧洲和韩国。在美国，CPL（电子竞技职业联盟）是电子竞技的主要推动者，与韩国的WCG、法国的ESWC（电子竞技世界杯）并称为世界三大电子竞技赛事。虽然韩国WCG在2014年停办，但是其曾经的辉煌仍旧给后来者已很多启发。因为欧美电子竞技商业模式较为相似，而与韩国电子竞技商业模式产别则比较大。前瞻产业研究院发布的《2015-2020年中国网络游戏行业商业模式创新与投资机会分析报告》将欧洲和美国的电子竞技商业模式合并分析。 图表：电子竞技商业模式比较——欧美模式VS韩国模式 图片来源：前瞻产业研究院 一、电子竞技客户价值主张：欧美个性化VS韩国精英化 在"客户价值主张"这个维度上，欧美赛事在理念上和文化差异上与韩国有较大差异，欧美电子竞技赛事以吸引更多人到现场参与活动为主要思路，其相应的客户价值主要指的是电子竞技赛事参与选手。欧美人更习惯亲自参与运动和活动，并在其中寻找自身的价值。这与欧美人崇尚个性自由，习惯亲自动手的文化习惯有关系；同时也与其自身的生活状态有关--欧美电子经济发达的国家多生活水平较高，有较多的业余时间和兴趣；另外，其生活方式和工作方式较亚洲人而言流动性比较大，因此大量参与人员可以方便地参与到不同地点准备得赛事，而用支付较高的成本。与此同时，美国是个更为多元化的社会，美国高校已经开始将电子竞技当作一项团队体育运动，美国政府也将职业电子竞技选手视作移民的一项条件，因此对于电子竞技的参与者而言参与比赛本身就是一种价值的体现，这也是欧美电子竞技基础广泛的根本原因。 而在韩国，电子竞技产业化更为深入，甚至成为了其国民经济的支柱产业之一。因为韩国的游戏开发商和硬件生产商一流厂商较少，韩国主要是依靠电视媒体作为主要的平台。1999年初，OGN以独立专业游戏电视台的姿态成立，标志着韩国在游戏领域有了自己的传播媒体。在此之前，韩国也曾举办过一些星际争霸比赛，可是OGN一开班，就拿出坚定地走职业化的决心，力图改变以往游戏比赛仅仅是电脑厂商促销活动或网吧宣传活动的尴尬局面。OGN争取到赞助商强力资金支持，将比赛放到了大型场馆，并在同时请来了世界上最优秀的玩家参加比赛，这一切都是为了通过电视台这种强势媒体向更多玩家呈现最高水准最具有观赏性的游戏对抗。电视台举办了赛制公平合理又引人入胜的比赛，选手们自然全力发