1、ICS 25.040.40 L 67 道昌中华人民主t/、和国国家标准G/T 20719. 12-201 O/ISO 18629-12: 2005 工业自动化系统与集成过程规范语言第12部分:外核Industrial automation systems and integration Process specification language一Part 12 Outer core CISO 18629-12: 2005 , IDT) 2011-01-14发布2011-06-01实施数码防伪中华人民共和国国家质量监督检验检亵总局中国国家标准化管理委员会发布GB/T 20719.12-2010
2、/ISO 18629-12:2005 目次前言.皿引言.凹1 范围2 规范性引用文件3 术语、定义及缩略语.13. 1 术语和定义3.2 缩略语.5 4 GB/T 20719概述5 GB/T 20719本部分的组织 5 6 子活动核心理论67 发生树核心理论88 离散状态核心理论119 原子活动核心理论1410 复杂活动核心理论.16 11 活动发生核心理论20附录A(规范性附录)SC 4标准中ASN.1标识符的应用27附录B(资料性附录)与情景演算的关系.28 附录C(资料性附录)使用PSL外核描述过程的实例附录NA(资料性附录)本部分英文黑体词的含义34参考文献. . . . . . .
3、. . . . . . . . . . . 35 索引I GB/T 20719.12-2010/ISO 18629-12 :2005 剧吕GB/T 20719(工业自动化系统与集成过程规范语言目前拟分为如下部分:一一第1部分z概述与基本原理;一一第11部分:PSL核心;第12部分z外核;一一第13部分:时序理论;一一第14部分:资源理论;一一-第15部分z活动性能理论;一一第21部分:EXPRESS; 第22部分:XML;第23部分:UML;一一第41部分:定义性扩展:活动扩展;二一第42部分:时间和状态;第43部分:定义性扩展:活动次序和持续时间扩展;二一第44部分:定义性扩展:资源扩展;一
4、一第45部分:资源集的种类;一一第46部分:加工活动;第47部分:过程目的。本部分为GB/T20719的第12部分。本部分等同采用IS018629-12: 2005(工业自动化系统与集成过程规范语言第12部分:外核(英文版)。本部分的技术内容和组成结构与IS018629-12: 2005相一致，在编写格式上符合GB/T1. 1 2000 标准化工作导则第1部分z标准的结构和编写规则。只是根据我国国家标准的制定要求和为方便使用，做了如下编辑性的改动z二一将IS018629改为GB/T20719，把IS018629-12改成GB/T20719. 12或GB/T20719 本部分。-一删除了IS01
5、8629-12 :2005的前言，并按照我国国家标准编制要求重新起草了前言。一-将IS018629-12: 2005第2章规范性引用文件中的引导语改为GB/T1. 1-2000中规定的引导语。一一IS018629-12: 2005标准中index的两个关键词manufacturingfacilities和satisfiable在原标准中没有找到，所以在中文索引中删除这两个关键词。一-将本部分中出现的己转化为国家标准的国际标准编号改为国家标准编号，便于使用和查阅。未转化的国际标准保留。为了使读者便于理解本部分黑体词的含义，增加了附录NA。一一删去了原文中不符合我国标准编写要求的字句。本部分附录A
6、为规范性附录;附录B、附录C、附录NA为资料性附录。本部分由中国机械工业联合会提出。本部分由全国自动化系统与集成标准化技术委员会CSAC/TC159)归口。本部分起草单位:北京机械工业自动化研究所、清华大学。本部分主要起草人:刘颖、黄双喜。阳山GB/T 20719.12-201 O/ISO 18629-12: 2005 引GB/T 20719是为了进行与制造过程相关的计算机可解释的信息交换所使用的国家标准。GB/T 20719标准包含的所有部分结合在一起，为描述贯穿整个生产过程的制造活动提供了一类语言(该生产过程可能限于一个工业公司，也可能跨越几个工业部门或公司)，并独立于任何特定的表示模型。
7、语言的本质使得它适用于在生产过程的各个阶段共享与制造相关的过程信息。GB/T 20719的本部分提供了国际标准中定义的语言的核心元素的描述。GB/T 20719中的所有部分与制造管理领域软件应用中采用的任何特定过程的表述或模型元关。本标准的所有部分一同为改善这些应用软件的协同性提供了一个结构框架。N GB/T 20719.12-2010/ISO 18629-12:2005 工业自动化系统与集成过程规范语言第12部分:外核1 范围GB/T 20719的本部分通过使用GB/T20719的一组公理和定义提供了属于PSL语言外核的概念表述。这些公理为GB/T20719外核中的术语提供了语义的公理化。G
8、B/T 20719本部分的范围包括:一一活动和子活动的集合;一一离散活动和状态;一一活动发生的约束;一一基本活动的并发;一一复杂活动;一一复杂活动的发生。2 规范性引用文件下列文件中的条款通过GB/T20719的本部分的引用而成为本部分的条款。凡是注日期的引用文件，其随后所有的修改单(不包括勘误的内容)或修订版均不适用于本部分，然而，鼓励根据本部分达成协议的各方研究是否可使用这些文件的最新版本。凡是不注日期的引用文件，其最新版本适用于本部分。GB/T 16262. 1 信息技术抽象语法记法一CASN. 1) 第1部分:基本记法规范CGB/T 16262.1-2006,ISO/IEC 8824-
9、1:2002 ,IDT) GB/T 16656. 1 工业自动化系统与集成产品数据表达与交换第1部分:概述与基本原理CGB/T 16656.1一2008，ISO10303-1: 1994 , MOD) GB/T 19114.1 工业自动化系统与集成工业制造管理数据第1部分:综述CGB/T19114.1 2003 ,ISO 15531-1:2002 ,IDT) GB/T 20719. 1 工业自动化系统与集成过程规范语言第1部分:概述与基本原理CGB/T 20719.1一2006，ISO18629-1: 2004 , IDT) GB/T 20719. 11 工业自动化系统与集成过程规范语言第11
10、部分:PSL核心CGB/T20719. 11-2010 ,ISO 18629-11: 2005 , IDT) 3 术语、定义及缩暗语3. 1 术语和定义下列术语和定义适用于GB/T20719的本部分。3. 1. 1 公理axiom 形式语言中的合式公式，用以对一门语言的词汇中的符号解释加以约束。GB/T 20719. 1J 3. 1. 2 保守定义conservative definition 指明充要条件的定义，充要条件是指术语应该满足并且不允许从该理论作出新的推论的条件。GB/T 20719. 1J GB/T 20719.12-2010/ISO 18629-12 :2005 3. 1. 3
11、 核心理论core theory 表示基本概念的关系符号和函数符号的公理集。GB/T 20719. 1的修改3.1.4 数据data 定义适合于人或计算机通信、解释或处理的形式化方法的信息表示。GB/T 16656. 1J 3. 1. 5 定义的词汇defined lexicon 非逻辑词汇的一系列符号，表示所定义概念。注:定义的词汇分为常量、函数和关系符号。示例:具有保守定义的术语。GB/T 20719. 1J 3.1.6 定义性扩展definitional extension 指PSL核心的扩展，它引入了完全由PSL核心定义的新的语言术语。注:定义性扩展为PSL核心增加了新的表达能力，但它
12、常常主义领域应用中的语义及术语。GB/T 20719. 1J 3.1.7 扩展extension 包含附加公理的PSL核心的扩充。注1:PSL核心是一组相对简单的公理，足以表达较广范围内的基本过程。然而，更复杂的过程所需的表达性资源超出了PSL核心的范围。相对于将每一个可能的概念(其对于描述个或另个过程可能有用)杂乱地添加j1j PSL核心中去，更好的方式是开发各种独立的、模块化的扩展，并把它们添加进PSL核心。采用这种方式，用户可以根据自己的表达需求精确地裁剪语言。注2:所有的扩展均为核心理论或定义性扩展。GB/T 20719. 1J 3. 1.8 语法grammar 说明如何将逻辑符号和词
13、汇术语组合为合式公式的规范。GB/T 20719. 1J 3. 1.9 事等idempotent 一个集合中的元素(a)在内部二元运算下(OP)具有:aOPa=a。注:对于函数，当定义域中的每个元素都是等等的，则函数是军等的。示例:集合理论交集和并集是等等的，因为S门S=S以及SUS=S。3. 1. 10 信息information 事实、概念或指令。GB/T 16656. 1J 3. 1. 11 2 解释interpretation 一个理论中所有命题的论域和真值(真或假)指派。注2请见附录C中解释的示例。GB/T 20719.12-2010/ISO 18629-12 :2005 3. 1.
14、 12 语言language 词汇和语法的结合。GB/T 20719. 1J 3. 1. 13 词汇lexicon 符号和术语的集合。注:词汇包括逻辑符号例如布尔连接和量词)与非逻辑符号。对于GB/T20719来说，词汇的非逻辑部分包括用于表达本体的基本概念的词语常量，函数符号与关系符号)。GB/T 20719. 1J 3. 1. 14 制造manufacturing 将原材料或半成品转换成成品的功能或行为。GB/T 19114. 1J 3. 1. 15 制造过程manufacturing process 一套结构化的行为或操作，它完成了将原材料或半成品向成品的转化。注:制造过程可被安排在程序
15、规划、产品规划、单元规划或装配位置规划里。根据战略性应用和物资的分配，制造过程可被用于支持按库存生产、按订单生产、按订单装配。GB/T 19114. 1J 3. 1. 16 模型model 满足一种理论中所有合式公式的一组元素和事实任务的合成。注1:模型这个词在逻辑中的用法不同于它在大多数科学及日常读物中的用法。如果一个命题在某种解释中为真，那么就可以说这种解释是该命题的模型。这里所说的语义常被称作模型理论语义。注2:模型一般表示为包含附加结构的集合(偏序，点阵，或向量空间)。模型定义了术语的含义以及本模型中所采用语言的命题的真值概念。给定一个模型，在公理集中使用的数学结构基本公理集就通过语言
16、及它们的逻辑关系成为概念论证的基础，因此模型的集合构成了本体的形式语义。GB/T 20719. 1J 3. 1. 17 本体ontology 按照词汇中术语的含义的某些规范而定的专门术语的词汇。注1:与形式语言中术语含义的规范一同给出的相关术语的结构化集合。术语含义的规范说明了术语为什么相关、如何相关，以及集合划分和构造的条件。注2:PSL(比如GB/T20719)的主要部分就是一个本体。基本概念就是本体论。通过GB/T20719可以描述基本制造工程及业务过程。注3:本体的核心不只是术语，也包括它们的含义。术语的任意集合包含在本体中，但只有在含义一致时这些术语才能被共享。共享的是术语的指定语义
17、，而不是简单的术语共享。注4:没有显式定义的任何术语都可能成为含糊及混乱的来源。本体论的难点是:需要建立一个框架以使框架中术语的含义清晰明确。对于GB/T20719这个本体，有必要提供一个过程信息的严格的数学特性描述以及GB/T 20719语言中信息的基本逻辑特性的精确表达。GB/T 20719. 1J 3. 1. 18 外核outer core 作为PSL核心扩展的核心理论的集合，在适用性中它具有很高的普遍性，因此专门预留出来。3 G/T 20719.12-2010/ISO 18629-12:2005 注2事实上，扩展包含了外核的公理。GB/T 20719. 1J 3. 1. 19 基本概念
18、primitive concept 没有保守定义的词汇术语。GB/T 20719. 1J 3. 1. 20 基本词汇primitive lexicon 表示基本概念的非逻辑词汇的符号集合。注:基本词汇分为常量、函数符号和关系符号。GB/T 20719. 1J 3. 1. 21 过程process 涉及各种企业实体的一套结构化的活动，是为特定的目的设计和组织的。注:这里所提供的定义和GB/T16656.49非常接近。然而GB/T19114需要一套结构化行为的观念，对于时间和步骤没有任何预先确定，另外，从流程管理的观点来看，为同一目的需要一些空过程，尽管实际上它们不起任何作用。GB/T 19114
19、. 1J 3. 1. 22 产晶product 由天然或人造而成的事物。GB/T 16656. 1J 3.1.23 证明论proof theory 解释某语言的语义所必需的理论与词汇元素的集合。注2它包含三部分:PSL核心，外核及扩展。GB/T 20719. 1J 3. 1. 24 PSL核心PSL-core 对于活动、活动发生、时间点、对象这些概念的公理的集合。注:PSL核心的动机是2任何两个过程相关的应用软件都需要共享这些公理，以交换过程信息，因此PSL核心足可用于描述制造过程的基本概念。这样，基本过程的特性描述就几乎无需那些超出描述这些过程所需的本质的假设了，因此PSL核心在逻辑表述方面
20、比较薄弱。尤其是，PSL核心并不够强大，它不能提供很多辅助概念的定义，而这些辅助概念是描述关于制造过程的所有感知事物所必需的。GB/T 20719. 1J 3. 1. 25 半格semilattice 在偏序中，每两个元素都具有一个唯一的最小上界。3. 1. 26 4 理论theory 属于给定概念和概念集的公理和定义的集合。注:这个定义反映了人工智能的方法，在此方法中理论是基于相关概念的含义的假设的集合。GB/T 20719. 1J GB/T 20719.12-2010/ISO 18629-12 :2005 3. 1. 27 讨论域universe of discourse 属于一个真实世界
21、领域的具体或抽象的事务的集合，根据其在模块化的系统和相应环境上的重要性进行选择。GB/T 19114. 1J 3.2 缩略语下列缩略语适用于GB/T20719的本部分。FOL 一阶逻辑First-Order Logic; BNF 巴克斯范式Backus-Naur Form; KIF 知识交换格式Knowledge Interchange Format; PSL 过程规范语言Process Specification Language 0 4 GB/T 20719概述GB/T 20719详细描述了一种用于表示过程信息的语言，即过程规范语言。它由用于过程描述的词汇、本体和语法组成。注1:PSL是一
22、种以数学定义良好的词表和语法为基础，用于详细描述制造过程的语言。这样，它不同于GB/T 16656 ,GB/T 17645 ,GB/T 19114和GB/T18975标准中使用的其他语言。就两个过程的信息交换而言，PSL确定了与其行为无关的每一个过程。例如，一个过程中被视为资源的对象可能与另一个过程中被视为产品的对象被识别为同一个对象。注2:PSL是以数学集合核心理论和情景演算(见附录因为基础的。这样，它采用的描述方法与使用GB/T16656 标准中定义的现存语言的方法显著不同。与其说PSL中这些概念的含义遵循定义术语的形式集合，不如说它们遵循公理与支持定义的集合。GB/T20719给出了相应
23、的注释及举例，以辅助对该语言的基本词汇的理解。GB/T 20719部分1x系列详细说明了得到GB/T20719的基本概念的精确定义和公理所需的核心理论，这些核心理论可以实现不同模式之间的精确语义翻译。以下各项属于GB/T20719. 1x的范畴:语言的基本要素的表示法;一一提供与足以描述基本过程所需的直觉语义基本概念相符的标准化公理集;一一发展遵循PSL核心的其他核心理论或扩展的规则集合。以下不属于GB/T20719. 1x的范畴:一一涉及非核心理论概念的信息表示法。5 GB/T 20719本部分的组织本条目详细说明了组成GB/T20719中本部分的基本理论。5. 1 外核的扩展构成GB/T2
24、0719本部分的核心理论有=一一子活动核心理论(subactivity.th) ; 一二发生树核心理论(occtree.th) ; 离散状态核心理论(disc_state.th) ; 一一原子活动核心理论(atomic.th) ; 复杂活动核心理论(complex.th); 活动发生核心理论(act_occ.th)。图1显示了外核中这些理论间的关系，图中的箭头表示这些理论间的从属关系。外核的所有理论都是PSL核心的扩展。原子活动核心理论是子活动理论和发生树理论两个理论的扩展，而离散状态核GB/T 20719.12-2010/ISO 18629-12:2005 心理论只是发生树核心理论的扩展。活
25、动发生核心理论是复杂活动核心理论的扩展，反之，复杂活动核心理论又是原子活动核心理论的扩展。圄1SL外核公理集合间的关系6 子活动核心理论子活动核心理论提供了流程组成的概念的公理。子活动发生次序理论的唯一强制约束是z子活动关系要与一个离散偏序同构。其他核心理论对其具有附加的强制约束。6. 1 子活动核心理论的基本关系子活动核心理论的非逻辑词汇包含一个基本关系符号:subactivity 0 6.2 子活动核心理论的定义关系子活动核心理论的非逻辑词汇包含一个定义关系符号:一一-pnmltlve。6.3 与其他公理集的关系子活动核心理论需要GB/T20719. 11 (PSL核心)中所详细说明的ps
26、l_core.tho 子活动核心理论不需要定义性扩展。6.4 子活动核心理论的非正式语义6. 4. 1 subactivity 用于su bacti vi ty的KIF符号是z(subactivity ?a1 ?a2) 用于subactivity的非正式语义是:当且仅当活动?a1是活动?a2的子活动时，(subactivity?a1 ?a2)在子活动核心理论的解释中为真。子活动关系在活动的集合上形成一个离散偏序。6. 4. 2 primitive 用于primitive的KIF符号是:(primitive ?a) 用于primitive的非正式语义是:当且仅当活动?a除它本身之外没有任何子活动
27、时，(primitive?a)在子活动核心理论的解释中为真。6.5 子活动核心理论中的定义当且仅当一个活动除它本身之外没有任何子活动时，该活动为基本。6 GB/T 20719.12-2010/ISO 18629-12:2005 6.5. 1 定义1(forall (?a) (iff (primitive ?a) (forall (?al) (irnplies (subactivity ?al ?a) ( = ?al ?a) 6.6 子活动核心理论的公理6.6. 1 公理1子活动是活动上的一个关系。(forall (?al ?a2) (irnplies 6.6.2 公理2子活动是自反的。(for
28、all (?a) (subactivity ?al ?a2) (and (activity ?al) (activity ?a2) (irnplies (activity?a) (subactivity ?a ?a) 6.6.3 公理3子活动是反对称的。(forall (?al ?a2) (irnplies (皿d6.6.4 公理4子活动是传递的。(forall (?al ?a2 ?a3) (subactivity ?al ?a2) (subactivity ?a2 ?al) ( = ?al ?a2) (irnplies (and (subactivity?al ?a2) 6.6.5公理5(s
29、ubactivity ?a2 ?a3) (subactivity ?al ?a3) 子活动关系是一个离散排序，故在排序中每一个活动都有一个向下的后继。(forall (?al ?a2) (irnplies 6.6.6 公理6(subactivity ?al ?a2) (exists (?a3) (and (subactivity ?al ?a3) (subactivity ?a3 ?a2) (forall (?a4) (irnplies (and (subactivity ?al ?a4) (subactivity ?a4 ?a3) (or ( = ?a4 ?al) (= ?a4 ?a3) 子
30、活动关系是个离散排序，故在排序中每一个活动都有一个向上的后继。7 GB/T 20719.12-2010/ISO 18629-12:2005 (forall (?al ?a2) (implies (subactivity ?al ?a2) (exists (?a3) (and (subactivity ?al ?a3) (subactivity ?a3 ?a2) (forall (?a4) (implies 7 发生树核心理论(and (subactivity ?a3 ?a4) (subactivity ?a4 ?a2) (or ( = ?a4 ?a2) (= ?a4 ?a3) 发生树是活动发生
31、的所有离散序列的集合。发生树与情景演算中情景树的子结构是同构的(见附录C)，其主要区别是2每个发生树具有一个唯一的初始活动发生，而不是唯一的初始情景。就像在情景演算中，引入了poss关系来实现对发生树中活动发生的约束的说明。因为发生树包含有域的建模者认为不可能发生的序列，所以poss关系就修剪掉了发生树上与这些不可能的活动发生相对应的分枝。需要注意的是，发生树并不是一个表达一个活动的子活动发生的结构。发生树并不表示一个活动的特定发生，它表示的是域中所有活动的全部发生。7. 1 基本关黑发生树的非逻辑词汇包含三个基本关系符号:earlier; 一一一initial;legal。7.2 基本函数发
32、生树的非逻辑词汇包含一个基本函数符号:一-一successor，7.3 与其他公理集的关系发生树核心理论需要GB/T20719. 11 (PSL核心)中所详细说明的psl_core.tb, 发生树核心理论不需要定义性扩展。7.4 发生树核心理论的非正式语义7.4. 1 earlier 用于earlier的KIF符号是:(earlier ?occl ?occ2) 用于earlier的非正式语义是:当且仅当两个活动发生?occl和?occ2位于树的同一个分枝上，并且?occl比?occ2更接近树的根时，(earlier?occl ?occ2)在发生树核心理论的解释中为真。在发生树的解释中，活动发生
33、的所有序列的集合形成一棵树;earlier(早于)关系详细说明了树中活动发生上的偏序。7. 4. 2 initial 8 用于initial的KIF符号是:(initial ?occ) 用于initial的非正式语义是:当且仅当活动发生?occ是发生树的根时，(initial?occ)在发生树核心理论的解释中为真。GB/T 20719.12-2010/ISO 18629-12:2005 7.4.3 legal 用于legal的KIF符号是:(legal ?occ) 用于poss的非正式语义是:当且仅当活动发生?occ是合法发生树的元素时，(legal?occ)在发生树核心理论的解释中为真。7.
34、4.4 poss 用于poss的KIF符号是:(poss ?occl ?occ2) 用于poss的非正式语义是:当且仅当活动?a具有一个合法发生，并且该合法发生是发生树中活动发生?occ的后继时，(poss?a ?occ2)在发生树核心理论的解释中为真。7. 4. 5 precedes 用于precedes的KIF符号是z(precedes ?occl ?occ2) 用于precedes的非正式语义是:当且仅当在发生树中，活动发生?occl早于活动发生?occ2，并且这两个活动发生之间的所有活动发生都对应于可能的活动时，(precedes?occl ?occ2)在发生树核心理论的解释中为真。该
35、关系详细说明了发生树的子树，其中每个活动发生都是可能的活动的发生。7. 4. 6 successor 用于successor的KIF符号是:(successor ?a ?occ) 用于successor的非正式语义是:当且仅当?occ2表示紧接在发生树中活动发生?occ之后的?a的发生时，(=(successor?a ?occ) ?occ2)在发生树核心理论的解释中为真。7.5 发生树核心理论的公理以下为发生树核心理论中的公理集。7.5. 1 公理1earlier(早于)关系受活动发生的约束。(forall (?occl ?occ2) (implies 7.5.2 公理2(earlier ?o
36、ccl ?occ2) (and Cactivity_occurrence ?occl) Cactivity_occurrence ?occ2) 发生上的earlier(早于)关系是反自反的。Cforall (?occl ?occ2) (implies Cearlier ?occl ?occ2) (not (earlier ?occ2 ?occl) 7.5.3 公理3发生上的earlierC早于)关系是传递的。(forall (?occl ?occ2 ?occ3) (implies (and (earlier ?occl ?occ2) (earlier ?occ2 ?occ3) (earlier
37、 ?occl ?occ3) 9 GB/T 20719. 12-2010/ISO 18629-12:2005 7.5.4 公理4发生树中的一个分枝是活动发生的一个全序集。(forall (?occl ?occ2 ?occ3) (implies (皿d(earlier ?occl ?occ2) (earlier ?occ3 ?occ2) (or (earlier ?occl ?occ3) (earlier ?occ3 ?occl) ( = ?occ3 ?occl) 7.5.5 公理5没有早于初始发生的发生。(forall (?occl ?occ2) (implies (ini tial ?occl
38、) (not (exists (?occ2) (arlier ?occ2 ?occl) 7.5.6 公理6发生树的每个分枝都有一个初始发生。(forall (?occl ?occ2) (imp1ies (earlier ?occl ?occ2) (exists (?occp) (and (initial ?occp) (or (earlier ?occp ?occl) (= ?occp ?occl) 7.5.7 公理7每个活动都有一个初始发生。(forall (?a) (implies (activity?a) (exists (?s) (皿d(occurrence_of?s ?a) (ini
39、tial ,?s) 7.5.8 公理8在发生树中，同一活动没有两个初始活动发生。(forall (?occl ,?occ2 ?a) (implies (and ( = ?occl ?occ2) (initial ?occl) (ini tial ?occ2) (occurrence_of ?occl ?a) (occurrence_of ?occ2 ?a) 7.5.9 公理910 一个活动发生的后继是该活动的一个发生。(forall (?a ?occ) (implies (and (activity_occurrence ?occ) (activity ?a) (occurrence_of (
40、successor ?a ?occ) ?a) G/T 20719.12-20 10/ISO 18629-12 :2005 7.5. 10 公理10每一个非初始发生都是另一个发生的后继。(forall ( ?occ) (implies 7.5. 11公理门(not (initial ?occ) (exists ( ?a ?occp) ( = ?occ (successor ?a ?occp) 当且仅当发生?occ2晚于?occl时，发生?occl先于?occ2的后继发生。(forall (?a ?occl ?occ2) (iff (earlier ?occl (successor ?a ?occ
41、2) (or (earlier ?occl ?occ2) ( = ?occl ?occ2) 7.5.12 公理12活动发生受legal(合法)关系的约束。(forall ( ?occ) (implies 7.5.13 公理13(legal ?occ) (activity_occurrence ?occ) 如果一个活动发生是合法的，那么在发生树中所有早于它的活动发生也是合法的。(forall ( ?occl ?occ2) (implies (and (legal ?occl) 7.5.14 公理14(earlier ?occ2 ?occl) (legal ?occ2) 一个活动发生的结束在其后继
42、的起始之前。(forall ( ?occl ?occ2) (implies (earlier ?occl ?occ2) (before (endof ?occl) (beginof ?occ2) 7.5. 15 定义1poss关系介于活动和活动发生之间。(forall ( ?a ?occ) (iff (poss ?a ?occ) (legal (successor ?a ?occ) 7.5.16 定义2当且仅当在排序关系中活动发生?occl早于另一个活动发生?occ2，并且它们之间的每一个活动发生都是可能的，这时活动发生?occl先于?occ2o(forall (?occl ?occ2) (i
43、ff (precedes ?occl ?occ2) (and (earlier ?occl ?occ2) Clegal ?occ2) 8 离散状态核心理论离散状态核心理论引入了状态流(fluent)的棋念。流仅通过活动的发生而改变，但流不在基本活动的发生过程中改变。此外，活动具有前提条件(一个发生之前必须保持的流)和效果(一个发生之后常要保持的流)。11 GB/T 20719.12-2010/ISO 18629-12:2005 8. 1 离散状态核心理论中的基本范畴离散状态核心理论的非逻辑词汇包含一个基本范畴:一一一-state。8.2 离散状态核心理论中的基本关系离散状态核心理论的非逻辑词汇
44、包含两个基本关系符号:一-holds;pnoro 8.3 与其他公理集的关系本核心理论需要zGB/T 20719. 11 (PSL核心)中所详细说明的psl_core.th; 十二occtree.th (发生树核心理论)。离散状态核心理论不需要定义性扩展。8.4 离散状态核心理论的非正式语义8.4. 1 state 用于state的KIF符号是:(state ?f) 用于state的非正式语义是:当且仅当?f为解释的论域中的状态集合的一个成员时，(state ?f)在离散状态核心理论的解释中为真。状态是对象的子范畴。注:对象在GB/T20719. 11中已被定义。状态直观地表示域中由于活动的发
45、生而变化的性质和关系。8.4.2 holds 用于holds的KIF符号是:(holds ?f ?occ) 用于holds的非正式语义是:当且仅当在活动发生?occ之后状态?f为真时，(holds?f ?occ)在离散状态核心理论的解释中为真。8.4.3 prior 用于pnor的KIF符号是:(prior ?f ?occ) 用于prior的非正式语义是:当且仅当在活动发生?occ之前状态?f为真时，(prior?f ?occ)在离散状态核心理论的解释中为真。8.5 离散状态核心理论的公理以下为离散状态核心理论中的公理集。8.5. 1 公理1状态是对象。(forall ( ?f) (impli
46、es (state ?f) (object ?f) 8.5.2 公理212 Holds关系仅介于状态和活动发生之间。直观上，它表示活动发生?o之后的状态为真。(forall ( ?f ?occ) GB/T 20719.12-2010/ISO 18629-12 :2005 (implies (holds?f ?occ) 8.5.3 公理3(and (state ?f) (activity_occurrence ?occ) pnor关系仅介于状态和活动发生之间。直观上，它表示活动发生?o之前的状态为真。(forall (?f ?occ) (implies (prior?f ?occ) 8.5.4
47、公理4(and (state ?f) (activity_occurrence ?occ) 对于所有的初始发生，在其之前所保持的状态是相同的。(forall (?occl ?occ2 ?f) (implies 8.5.5 公理5(and (initial ?occl) (initial ?occ2) (iff (prior ?f ?occl) (prior ?f ?occ2) 当且仅当在一个状态在一个发生的后继发生之前一直保持着时，该状态在该发生之后一直保持着。(forall (?a ?occ) (iff (holds?f ?occ) (prior ?f (successor ?a ?occ) 8.5.6 公理6如果一个流在某个活动发生后保持着，那么在保持该流的分枝中存在一个最早的活动发生。(forall (?f ?occl
