1、ICS 25.040.40 L 67 程自中华人民和国国家标准GB/T 20719.13-2010/ISO 18629-曰:2006工业自动化系统与集成过程规范语言第13部分:时序理论Industrial automation systems and integration Process specification language-Part 13: Duration anrl ordering theo.ries (ISO 18629-13: 2006 , IDT) 2010-09-02发布2010-12-01实施童生蚂防伪中华人民共和国国家质量监督检验检菇总局中国国家标准化管理委员会发布
2、GB/T 20719.13-201 O/ISO 18629-13: 2006 目次前言.1 引言.1I 1 范围-2 规范性引用文件3 术语、定义及缩略语14 GB/T 20719概述 4 5 GB/T 20719本部分的组织 5 6 子活动发生次序核心理论57 周期理论.7 8 发生树自同构139 活动包络理论附录A(规范性附录)在SC4标准中使用抽象语法符号1(ASN. 1)标识符18附录B(资料性附录)使用GB/T20719第13部分描述过程的实例参考文献索引GjT 20719.13-201 OjISO 18629-13: 2006 目。吕GBjT 20719工业自动化系统与集成过程规范
3、语言分为:第1部分:概述和基本原理;第11部分:PSL核心;第12部分:外核;一一第13部分:时序理论;一一第14部分:资源理论;一一第15部分:活动性能理论;一一第21部分:EXPRESS; 一一第22部分:XML;第23部分:UML;第41部分:活动;第42部分:时间和状态;第43部分:序列;一一第44部分:定义性扩展资源扩展;一一一第45部分:资源集的种类;一一第46部分:加工活动;一一第47部分:过程目的。本部分为GBjT20719的第13部分。本部分等同采用ISO18629-13: 2006工业自动化系统与集成过程规范语言第13部分:时序理论)(英文版)。本部分的技术内容和组成结构与
4、ISO18629-13: 2006相一致，在编写格式上符合GBjT1. 1 2000。只是根据我国国家标准的制定要求和为方便使用，做了如下编辑性的改动:一一将ISO18629改为GBjT20719，把ISO18629-13改成GBjT20719. 13或GBjT20719 本部分;一一删除了ISO18629-曰:2006的前言，并按照我国国家标准编制要求重新起草了前言;将ISO18629-13: 2006第2章规范性引用文件中的引导语改为GBjT1. 12000中规定的引导语。一将本部分中出现的已转化为国家标准的国际标准编号改为国家标准编号，便于使用和查阅。未转化的国际标准保留。一一删去了原文
5、中不符合我国标准编写的字句。一一一ISO18629-13 (英文版)索引中的satisfiable在原文中没有找到，所以在英文和中文索引中都删除了。本部分的附录A是规范性附录，附录B是资料性附录。本部分由中国机械工业联合会提出。本部分由全国自动化系统与集成标准化技术委员会(SACjTC159)归口。本部分由北京机械工业自动化所负责起草。本部分主要起草人:黎晓东、杨书评、刘颖。I GB/T 20719.13-2010/ISO 18629-13:2006 引GB/T 20719是为了进行与制造过程相关的计算机可解释的信息交换所使用的国家标准。GB/T 20719标准包含的所有部分结合在一起，为描述
6、贯穿整个生产过程的制造过程提供了一类语言(该生产过程可能位于一个工业公司，也可能跨越几个工业部门或公司)，并独立于任何特定的表示模型。语言的本质使得它适用于在生产过程的各个阶段共享与制造相关的过程信息。GB/T 20719的本部分提供了GB/T20719中定义的语言的核心元素的描述。GB/T 20719中的所有部分与制造管理领域软件应用中采用的任何特定过程的表述或模型无关。本标准的所有部分一同为改善这些应用软件的协同性提供了一个结构框架。H GB/T 20719.13-2010/150 18629-13: 2006 1 范围工业自动化系统与集成过程规范语言第13部分:时序理论GB/T 2071
7、9的本部分提供了与活动的次序和周期约束相关的基本棋念的表述，其范围如下:一一一子活动发生次序;一一周期;一一迭代发生次序;一一发生树自同态;一一活动包络。2 规范性引用文件下列文件中的条款通过GB/T20719的本部分的引用而成为本部分的条款。凡是注日期的引用文件，其随后所有的修改单(不包括勘误的内容)或修订版均不适用于本部分，然而，鼓励根据本部分达成协议的各方研究是否可使用这些文件的最新版本。凡是不注日期的引用文件，其最新版本适用于本部分。GB/T 16262.1 信息技术抽象语法记法一CASN.1)第1部分:基本记法规范CGB/T16262. 1-2006 ,ISO/IEC 8824-1:
8、 2002 , IDT) GB/T 19114.1 工业自动化系统与集成工业制造管理数据第1部分:综述CGB/T19114.1-2003 ,ISO 15531-1:2002 ,IDT) GB/T 20719.1 工业自动化系统与集成过程规范语言第1部分:概述与基本原理CGB/T 20719.1-2006 ,ISO 18629-1:2004,IDT) ISO 18629-11: 2005 工业自动化系统与集成过程规范语言第11部分:PSL核心ISO 18629-12 工业自动化系统与集成过程规范语言第12部分:外核3 术语、定义及缩略语3.1 术语和定义下列术语和定义适用于GB/T20719的本
9、部分。3. 1. 1 自同构automorphism 保留了某个模型中的关系和函数的集合上的元素的一一映射。3.1.2 公理axiom 形式语言中的合式公式，用以对一门语言的词汇中的符号解释加以约束。GBjT 20719. 1J 3. 1. 3 交换群commutative group 在内部二元运算COP)下具有:aOPb=bOPa的代数结构。1 GB/T 20719.13一2010/ISO18629-13:2006 3. 1.4 保守定义conservative definition 该定义指明一个术语应该满足的充分必要条件，并且不允许从该理论作出新的推论。GB/T 20719. 1的修改
10、3.1.5 核心理论core theory 表示基本概念的关系符号和函数符号的公理集。GB/T 20719. 1的修改3.1.6 定义的词汇defined lexicon 非逻辑词汇的一系列符号，表示所定义概念。注:定义的词汇分为常盘、函数和关系符号。示例:具有保守定义的术语。GB/T 20719. 1J 3. 1. 7 自同态endomotphism 一个集合到子集的映射，该子集保留了某个模型中的关系和函数3.1.8 扩展extensio. 包含附加公理的PSL核心的扩充。注1:PSL核心是一组相对简单的公理，足以表达较广范围内的基本过程。然而，更复杂的过程所需的表达性资源超出了PSL核心的
11、范围。相对于将每一个可能的概念(其对于描述个或另一个过程可能有用)杂乱地添加到PSL核心中去，更好的方式是开发各种独立的、模块化的扩展，并把它们添加进PSL核心。采用这种方式，用户可以根据自己的表达需求精确地裁剪语言。注2:所有的扩展均为核心理论或定义性扩展。GB/T 20719. (! 3. 1.9 语法graID:clar 说明如何将逻辑符号和词汇术t组合为合式公式的规范。GB/T 20719. 1J 3. 1. 10 同态homomorphism 在集合的元素上保留某种关系的集合之间的映射。3. 1. 11 . 解释interpretation 将真值(真或假)赋给该理论中所有语句的赋值
12、过程和论域。ISO 18629-11J 3.1.12 语言language 词汇和语法的结合。GB/T 20719. 1J 3. 1. 13 2 词汇lexicon 符号和术语的集合。注:词汇包括逻辑符号(例如布尔连接和址词)与非逻辑符号。对于GB/T20719来说，词汇的非逻辑部分包括用于表达本体的基本概念的词语(常盐、函数符号与关系符号)。G/T 20719.13-201 O/ISO 18629-13: 2006 GB/T 20719. 1J 3. 1. 14 模型model 满足一种理论中所有合式公式的一组元素和事实任务的合成。注1:模型这个词在逻辑中的用法不同于它在大多数科学及日常读物
13、中的用法:如果一个命题在某种解释中为真，那么就可以说这种解释是该命题的模型。这里所说的语义常被称作模型理论语义。注2:模型一般表示为包含附加结构的集合(偏序，点阵，或向量空间)。模型定义了术语的含义以及本模型中所采用语言的命题的真值概念。给定一个模型，在公理集中使用的数学结构基本公理集就透过语言及它们的逻辑关系成为概念论证的基础，因此模型的集合构成了本体的形式语义。GB/T 20719. 1J 3. 1. 15 单同态monomorphism 在集合的元素上保留某种关系的一一映射。3. 1. 16 本体ontology 按照词汇中术语的含义的某些规范而定的专门术语的词汇。注1:与形式语言中术语
14、含义的规范一同给出的相关术语的结构化集合。术语含义的规范说明了术语为什么相关、如何相关，以及集合划分和构造的条件。注2:过程规范语言(比如GB/T20719)的主要部分就是一个本体。通过GB/T20719，本体中的基本概念可以充分描述基本的制造过程、工程过程及商业过程。注3.本体的核心不只是术语，也包括它们的含义。术语的任意集合包含在本体中，但只有在含义一致时这些术语才能被共享。共享的是术语的指定语义，而不是简单的术语共享。注4:没有显式定义的任何术话都可能成为含糊及混乱的来源。本体论的难点是:帘要建立一个框架以使框架中术语的含义清晰明确。对于GB/T20719这个本体，有必要提供一个过程信息
15、的严格的数学特性描述以及GB/T 20719语言中信息的基本逻辑特性的精确表达。GB/T 20719. 1J 3. 1. 17 外核Outer Core 作为PSL核心扩展的核心理论的集合，在适用性中它具有很高的通用性和普适性，因此专门预留出来。注:实际上，扩展并入了外核的公理。GB/T 20719. 1J 3. 1. 18 基本概念primitive concept 没有保守定义的词汇术语。GB/T 20719. 1J 3. 1. 19 基本词汇primitive lexicon 表示基本概念的非逻辑词汇的符号集合。注:基本词汇分为常量、函数符号和关系符号。GB/T 20719. 1J 3.
16、 1. 20 过程process 为了一个既定目标而进行规划和组织的涉及各种企业实体活动的结构化集合。注:这里提出的定义与GB/T16656. 490S0 10303-49，IDT)中给出的定义非常接近。不过，GB/T19114需要的是活动的结构化集合的概念，对于时间或步骤不进行任何预先确定。另外，从流管理的观点来看，为了保持同步可能会帘要一些空白过程，尽管这些空白过程实际上什么也没做(ghosttask幽灵任务)。3 GB/T 20719.13-2010/ISO 18629-曰:2006GB/T 19114.1二2003J3. 1. 21 证明论proof theory 解释某语言的语义所必
17、需的理论与词汇元素的集合。注:它包含三部分:PSL核心，外核及扩展。GB/T 20719. 1J 3. 1. 22 PSL核心PSL-Core 对于活动、活动发生、时间点、对象这些概念的公理的集合。注:PSL核心的动机是:任何两个过程相关的应用软件都需要共享这些公理，以交换过程信息，因此PSL核心足可用于描述制造过程的基本概念。这样，基本过程的特性描述就几乎无需那些超出描述这些过程所需的本质的假设了，因此PSL核心在逻辑表述方面比较薄弱。尤其是，PSL核心并不够强大，它不能提供很多辅助概念的定义，而这些辅助概念是描述关于制造过程的所有感知事物所必需的。GB/T 20719. 1J 3.1.23
18、 理论theory 属于给定概念和概念集的公理和定义的集合。注2这个定义反映了人工智能的方法，它的理论是一个假定的集合(基于相关概念的含义)。GB/T 20719. 1J 3. 1. 24 论域universe of discourse 通过对感兴趣的建模系统以及相应环境进行选择，来实现对属于真实世界领域的具体或抽象事物的收集。GB/T 19114. 1 -2003J 3.2 缩略语下列缩略语适用于GB/T20719的本部分。一-FOL First-Order Logic 一阶逻辑;一BNF Backus-aur form 巳克斯范式;KIF Knowledge Interchange For
19、mat 知识交换格式;一-PSLProcess Specification Language 过程规范语言。4 GB/T 20719概述如GB/T20719. l(idt ISO 18529-1)所述，作为一个整体，GB/T2071S(idt IS0 18629)详细描述了一种用于表示过程信息的语言(叫做PLS的过程规范语言)。它由ISO186291)的第1119部分和第4149部分中用于过程描述的词汇、本体和语法组成。注1:PSL是一种以数学定义良好的词表和语法为基础，用于详细描述制造过程的语言。因此，它不同于EXPRESS(在GB/T16656. 11中被定义)语言以及GB/T16656.
20、 41 , GB/T 16656.钮，GB/T16656.49 , GB/T 17645 ,GB/T 19114.1-2003和GB/T18975中使用的语言，那些是模型语言。就两个过程之间的信息交换而言，PSL确定了与其行为无关的每一个过程。例如，一个过程中被视为资源的对象可能与另一个过程中视为产品的对象被识别为同一个对象。PSL以数学集合论和情景演算为基础(见ISO18629-11:2005附录D)。IS0 18629的第1119部分详细说明了得到ISO18629的基本概念的精确定义及相应公理所需的核心理论，这些核心理论可以实现不同模式之间的精确语义翻译。IS0 18629的第1119部分
21、提供:1) 某些部分正在开发中。4 G/T 20719.13-2010/ISO 18629-13:2006 语言的基本元素的表示法;二一与足以描述基本过程的直觉语义基本概念相应的标准化公理集;发展遵循PSL核心的其他核心理论或扩展(如第4149部分所提供的扩展)的规则集合。5 G/T 20719本部分的组织本条目详细说明了组成GB/T20719中本部分的基本理论。构成GB/T20719本部分的核心理论有:-一一子活动发生次序理论(soo.th);一一-周期理论(duration.th); 发生树自同构理论(preserve.th) ; 一一活动包络理论(envelop巳.th); GB/T 2
22、0719中本部分的全部理论是IS018629-12中理论的扩展。6 子活动发生次序核心理论子活动发生次序理论引入了表示一个复杂活动中子活动发生上的过程流和偏序的直觉知识所必需的概念。6.1 子活动发生次序理论的基本关系子活动发生次序理论的非逻辑词汇包含两个基本关系符号:二子活动发生次序理论的非逻辑词汇包含一个基本函数符号:soomapo 6.2 子活动发生次序理论的定义关系子活动发生次序理论的非逻辑词汇包含以下定义关系符号:root_soo; 一一一leaf_soo;一一-next_subactivity。6. 3 与其他公理集的关系子活动发生次序理论需要以下核心理论:一一-psl_core.
23、th; 一一一occtree.th; 一一atomic.th; 一complex.th; actocc. th。子活动发生次序理论不需要定义性扩展。6.4 子活动发生次序理论的非正式语义6.4. 1 soo 用于soo的KIF符号是:(soo ?s ?a) 用于soo的非正式语义是:当且仅当活动发生?s是活动汩的子活动发生次序的一个元素时，也00?s ?a)在子活动发生次序理论的解释中为真。6. 4. 2 soo_precedes 用于基本的KIF符号是:5 GB/T 20719.13-2010/ISO 18629-13:2006 ( soo _precedes ? s 1 ? s2 ? a)
24、 用于soo_precedes的非正式语义是:当且仅当在活动?a的子活动发生次序中，活动发生?s1先于活动发生?s2时，(soo _ precedes ? s 1 ?s2 ?a)在子活动发生次序理论的解释为真。这一关系定义了复杂活动的子活动发生上的一个偏序。6. 4. 3 soomap 用于soomap的KIF符号是:(soomap ?s) 用于soomap的非正式语义是:当且仅当活动发生?s1是与?s对应的子活动发生次序的元素时，(=?s1 (soomap ?s)在子活动发生次序理论的解释中为真。6.5 子活动发生次序理论中的定义6.5.1 定义1(与root_soo相关)当且仅当一个活动发
25、生是活动?a的子活动发生次序的一个元素，并且在该次序中没有先于它的活动发生时，这个活动发生是该子活动发生次序的根。(forall (?s ?a) (iff (root_soo ?s ?a) (and (soo ?s ?a) (not (exists (?s1) (soo_precedes ?s1?s ?a) 6.5.2 定义2(与leaf_soo相关)当且仅当一个活动发生是活动?a的子活动发生次序的一个元素，并且在该次序中没有活动发生位于它之后时，这个活动发生是该子活动发生次序的叶。(forall (?s ?a) (iff Cleaf soo ?s ?a) (and (soo ?s ?a) (
26、not (exists (?s1) (soo_precedes ?s ?s1 ?a) 6.5.3 定义3(与next_soo相关)在?a的子活动发生次序中，当且仅当活动发生?s1先于活动发生?s2，并且这两个活动发生之间没有子活动发生存在时，活动发生?s2是紧接在活动发生?s1之后的下一个子活动发生。(forall (?s1 ?s2 ?a) (iff (next soo ?s1 ?s2 ?a) (and (soo_pr巳cedes?s1 ?s2 ?a) (not (exists (?s3) (and (soo_precedes ?s1 ?s3 ?a) (soo_precedes ?s3 ?s2
27、 ?a) 6.6 子活动发生次序理论的公理6.6.1 公理1soo_precedes关系对子活动发生次序的元素进行了排序。(forall (?s1 ?s2 ?a) Cimplies (soo_precedes ?s1 ?s2 ?a) (and (soo ?s1 ?a) (soo ?s2 ?a) 6.6.2 公理26 子活动发生次序的元素是活动树的元素。(forall (?a ?s) (implies (soo?s ?a) GB/T 20719.13-2010/ISO 18629-13 :2006 (or (root ?s ?a) (exists (?s1) (min_precedes ?sl
28、?s ?a) 6.6.3 公理3soomap函数将活动树映射到子活动发生次序。(forall (?s ?a) (soo (soomap ?s) ?a) 6.6.4 公理4子活动发生次序的元素由soomap函数确定。(forall (?s ?a) (implies (soo?s ?a) (= ?s (soomap ?s) 6.6.5 公理5soomap函数是一个分支单同态。(forall (?s ?a) (or (mono (?s (soomap ?s) ?a) (= ?s (soomap ?s) 6.6.6 公理6活动树对于子活动发生次序是序同态。(forall (?a ?sl ?s2) QU
29、 E- aFEA -P飞m 飞(min_precedes ?sl ?s2 ?a) (soo_precedes (soomap ?sl) (soomap ?s2) ?a) (not (exists (?s3 ?s4) (and (min_precedes ?s4 ?s3 ?a) (= (soomap ?s3) (soomap ?sl) (= (soomap ?s4) (soomap ?s2) 6.6.7 公理7soo_precedes是不对称的。(forall (?a ?sl ?s2) (implies (soo_precedes ?sl ?s2 ?a) (not (soo_precedes ?
30、s2 ?sl ?a) 6.6.8 公理8soo _precedes是传递的。(forall (?a ?sl ?s2 ?s3) (implies (and (soo_precedes ?sl ?s2 ?a) (soo_precedes ?s2 ?s3 ?a) (soo_precedes ?sl ?s3 ?a) 7 周期理论周期理论引入了周期的概念。它通过将每一个点对映射到一个满足向量空间公理的叫做时间周期的新的对象子类上来的方法对时间线进行度量。7.1 周期理论中的基本关系周期理论的非逻辑词汇包含两个基本关系符号:一一timeduration(时间周期); 7 GB/T 20719.13-201
31、0/ISO 18629-曰:2006一一lesser(小于)。7.2 基本函数和常数周期理论的非逻辑词汇包含三个函数符号:-duration(周期); add(力日); mult(乘)。周期理论的非逻辑词汇包含四个常数符号:一一zero(零); -one(一); 二max+(最大); max一(最小)。7.3 周期理论的定义关系周期理论的非逻辑词汇包含一个定义关系符号:time_add(时间增加)。7.4 与其他公理集的关系周期理论需要:一-psl_core.th. 周期理论不需要定义性扩展。7.5 周期理论的非正式语义7.5. 1 timeduration(时间周期)用于timedurati
32、on的KIF符号是:(timeduration ?d) 用于timeduration的非正式语义是:当且仅当在解释的论域中?f是时间周期集合的成员时，(timeduration ?d)在周期理论的解释中为真。时间周期是对象的子范畴。7.5.2 lesser(小于)用于lesser的KIF符号是:Clesser ?dl ?d2) 用于lesser的非正式语义是:所有的时间周期都是线性有序。当且仅当时间周期?dl的值小于时间周期?d2的值时，Clesser?dl ?d2)在周期理论的解释中为真。7.5.3 duration(周期)用于duration的KIF符号是:(duration ?tl ?t
33、2) 用于duration的非正式语义是:当且仅当?d表示时间周期，并且该时间周期的值为时间线上时间点?tl和?t2之间的距离时，(=(duration ?tl ?t2) ?d)在周期理论的解释中为真。7.5.4 time_add(时间增加用于timeadd的KIF符号是:(time add ?t ?d) 用于time_add的非正式语义是:当且仅当?t2表示时间点，并且在时间线上从时间点?t到该时间点的距离为?d时，(= (time_add ?t?d) ?t2)在周期理论的解释中为真。7.5.5 add(1J日)用于add的KIF符号是:8 G/T 20719.13-2010/ISO 186
34、29-13:2006 (add ?dl ?d2) 用于add的非正式语义是:当且仅当?d3表示时间周期，并且该时间周期的值为时间周期?dl和?d2的值之和时，(=(add ?dl ?d2) ?d3)在周期理论的解释中为真。7.5.6 mult(乘)用于mult的KIF符号是:(mult ?x ?d) 用于mult的非正式语义是:当且仅当?d2表示时间周期，并且该时间周期的值为时间周期刊和?x(?x是一个交换群的元素)的值的乘积时，(= (mult ?x ?d) ?d2)在周期理论的解释中为真。7.5.7 zero(零)用于zero的非正式语义是:zero表示时间周期常数，它是add函数的加法单
35、位元素。7.5.8 one(一)用于one的非正式语义是:one表示时间周期常数，它是mult函数的乘法单位元素。7.5.9 max+(最大)用于max+的非正式语义是:max十是最大时间周期。7.5.10 max一(最小)用于max一的非正式语义是:max一是最小时间周期。7.6 周期理论的定义time_add(时间增加)函数将时间点?tl和时间周期?d映射到时间点?t2，这样?tl和?t2之间的周期为?d。(forall (?tl ?t2 ?d) (iff(= ?t2 (time add ?tl ?d) (and (timepoint ?tl) (timepoint ?t2) (timed
36、uration ?d) (= ?d (duration ?t2 ?tl) 7. 7 周期理论的公理以下为周期理论的公理集:7.7.1 公理1zero，max+和max一都是时间周期。(and (timeduration zero) (timeduration max+) (timeduration max-) 7.7.2 公理2两个时间周期相加的结果还是一个时间周期。(forall (?dl ?d2) (implies (and (timeduration ?dl) (timeduration ?d2) (timeduration (add ?dl ?d2) 9 G/T 20719.13-20
37、10/150 18629-13: 2006 7.7.3 公理3add函数是可结合的。Cforall C?dl ?d2 ?d3) Cimplies Cand Ctimeduration ?dl) C timeduration ?d2) Ctimeduration ?d3) C= Cadd Cadd ?dl ?d2) ?d3) Cadd ?dl Cadd ?d2 ?d3) 7.7.4 公理4zeroC零)是加法单位元素。C forall C? d) Cimplies Ctimeduration ?d) C = Cadd ?d zero) ?d) 7.7.5 公理5与一个时间周期相对的依然是一个时间
38、周期。Cforall C?dl) Cimplies Ctimeduration ?dl) Cexists C?d2) Cand Ctimeduration ?d2) C= (且dd?dl ?d2) zero) 7.7.6 公理6add函数是可交换的。Cforall C?dl ?d2) Cimplies Cand (timeduration ?dl) C timeduration ?d2) C = Cadd ?dl ?d2) Cadd ?d2 ?dl) 7.7.7 公理7时间周期与标量值的乘权还是时间周期。Cforall C?d ?r) Cimplies Ctimeduration ?d) Ct
39、imeduration Cmult ?r ?d) 7.7.8 公理8时间周期可以与标量相乘:Cforall C?dl ?d2 ?r) C= Cmu1t ?r Cadd ?dl ?d2) (add Cmult?r ?dl) Cmult?r ?d2) 7.7.9 公理9时间周期和标量的乘法是可分配的:Cforall C?d ?r ?s) C= CmultCadd?r?s) ?d) CaddCmu1t ?r?d) Cmult?s?d) 7.7.10 公理10时间周期和标量的乘法是可结合的。Cforall C?d ?r ?s) C= Cmult Cmult?r ?s) ?d) Cmult?r Cmul
40、t?s ?d) 7. 7. 11 公理11One(一)是乘法单位元素。10 GB/T 20719.13-201 O/ISO 18629-13: 2006 (forall (?d) (= ?d (mult one ?d) 7.7. 1-2 公理12时间周期的add函数在时间周期上保留lesser(小于)次序。(forall (?dl ?d2 ?d3) (and (timeduration ?dl) (timeduration ?d2) (timeduration ?d3) (iff (1esser ?dl ?d2) (1 esser (add ?dl ?d3) (add ?d2 ?d3) 7.7
41、.13 公理13如果两个时间周期是相等的，那么它们与另一个时间周期相加的结果也将相等。(forall (?dl ?y ?z) (and (timeduration ?dl) (timeduration ?d2) (timeduration ?d3) (iff (= ?dl ?d2) (= (add ?dl ?d3) (add ?d2 ?d3) 7.7.14 公理14max一小于任一时间周期，max+大于任一时间周期。(forall (?d) (implies (timeduration ?d) (and (1 esser ?d max+) (1esser max- ?d) 7.7.15 公理1
42、5除max+以外的任一周期与max一相加的结果仍是max一，反之亦然，max+与max一之和为零。(forall (? d) (implies (timeduration ?d) (and (implies (not (= ?d max一)(= max+ (add?d max+) (implies (not (= ?d max+) (= max一(add?d max一)(= zero (add max十max-)7.7.16 公理16周期函数为每一对时间点指定一个时间周期。(forall (?tl ?t2) Cimplies (and (timepoint ?t1) (timepoint ?t
43、2) (timeduration (duration ?tl ?t2) 7.7.17 公理17每个时间周期都与某一对时间点的周期函数值相等。(forall (? d) (implies (timeduration ?d) (exists (?tl ?t2) (and (timepoint ?tl) (timepoint ?t2) 11 GB/T 20719.13-2010/ISO 18629-曰:2006(= ?d (duration ?t1 ?t2) 7.7. 18 公理18当且仅当两个时间点相等时，周期函数的值为零。(forall (?t1 ?t2) (implies (and (time
44、point ?tl) (timepoint ?t2) (iff (= zero (duration ?t1 ?t2) (= ?t1 ?t2) 7.7.19 公理19?t1和?t2之间的周期函数值是1t2和?t1之间的周期函数值的加法逆元。(forall (?t1 ?t2) (implies (and (timepoint ?t1) (timepoint ?t2) (= zero (add (duration ?t1 ?t2) (duration ?t2 7t1) 7.7.20 公理20给定一个时间点7t1(不包括inf和inf十)，从?t1到任一时间点的周期是唯一的。(forall (?t1
45、?t2 7t3) (implies (and (timepoint?t 1) (tim叩oint?t2) (timepoint ?t3) (not (= ?t1 inf一) (not (= ?t2 inf十) (= (duration ?t1 ?t2) (dura tion ?tl ?t3) (= ?t3 ?t2) 7.7.21 公理21从任一点(不包括inf-)到inf的周期是max一，从任一点(不包括inf+)到inf十的周期是max十。(forall (?t) (and (implies (and (timepoint 7t) (not (= ?t inf ) ) (= max十(dur
46、ationini一?t) (implies (and (timepoint ?t) (not (= ?t inf十)(= max- (duration inf+ ?t) 7.7.22 公理22从inf一到任一点(不包括inf一)的周期是max+，从inf十到任一点(不包括inf十)的周期是口lax一-。12 forall (?t) (and (implies (and (timepoint ?t) (not (= ?t inf一)(= max一(duration?t inf一)(implies (and (timepoint ?t) (not (= ?t inf+) (= max十(durat
47、ion?t inf十)GB/T 20719.13-201 O/ISO 18629-13: 2006 8 发生树自同构发生树自同构核心理论对发生约束的直觉知识进行公理化，在该约束中:一个活动的合法发生依赖于其他活动的发生。8. 1 发生树自同构理论的基本关系发生树自同构的非逻辑词汇包含一个基本关系符号:-ubiquitous 。8.2 发生树自同构理论的定义关系发生树自同构的非逻辑词汇包含三个定义关系符号:一一end_iso;一二一legal_map;一一-tree_map。8.3 与其他公理集的关系本核心理论需要:-pslcore. th; 一一一occtree.th; 一一atomic.th; 二-complex.th I 一-actocc.tho 需要的定义性扩展是:一-一occ_precond.def。8.4 发生树自同构理论的非正式语义8. 4. 1 ubiquitous 用于ubiquitous的KIF符号是:(ubiquitous ?且1?a2) 用于ubiquitou色的非正式语义是:当且仅当?a1的京生树自同构保留的活动发生是，?a2的发生的子活动发生时，Cubiquitous?a1 ?a2) 在发生树自同构理论的解释中为真。8. 4. 2 end iso 用于endiso的KIF符号是:/ Cend_iso ?sl ?s2 ?s3
