论文部分内容阅读
描述逻辑是一种适合表示结构化数据的形式语言.通过将某种数据模型表示到描述逻辑，可以利用描述逻辑本身的推理机制对数据模型满足的各种性质进行推理，并为各种异构的数据模型提供统一的底层逻辑描述.辅以特定领域的本体知识，可以对领域知识库进行各种约束的推理和形式验证.本文主要研究关系数据模型的描述逻辑表示。
关系数据模型是一种具有代表性的数据模型，它是现有多种应用数据库系统的重要理论基础.关系数据模型将数据进行结构化表示，提供了一类完整性约束和函数依赖来描述数据具有的性质，并为结构化数据提供了一组称为关系代数运算的操作.从逻辑的视角，一个数据库可以被视作一个一阶理论，以及一阶理论上的一个解释.从一阶理论的角度看，完整性约束，函数依赖和关系代数运算可以视作一阶语言中的定理，利用一阶逻辑的推理机制进行推导.从解释的角度看，数据库视作一个模型，而完整性约束，函数依赖和关系代数运算对应的公式可以在模型中根据语义定义取真值或假值。
已有的工作并没有将关系数据模型的如上几个方面在一个统一的逻辑架构内进行表示.本文构建一种多类动态描述逻辑DMDL，将关系数据模型中的数据以及数据满足的各种完整性约束和函数依赖等等断言在DADL中进行表示，并利用DMDL的动态算子对关系代数运算进行表示。
关系数据模型的描述逻辑表示本质上是形式系统之间的翻译，而对形式系统间翻译的各种逻辑性质的研究是很重要的.已有的翻译逻辑性质的研究多是基于两个逻辑间的翻译，这样我们首先需要给出从关系数据模型到描述逻辑的翻译正确性的形式定义，再对其进行证明，从而保证翻译合理地将关系数据库的各方面信息转化到描述逻辑中。
本文的主要工作包含如下几个方面：
1.构造了一种多类的动态描述逻辑DMDL.DMDL的多类机制对不同类型的个体和概念进行了区分，避免了一类在关系数据库中无意义的描述逻辑公式的出现。DMDL提供一组动态算子，并以语法中的关系概念作为动态算子的参数，以此对关系数据模型的动态行为，即关系代数运算进行表示。
2.构造了从关系数据模型到动态描述逻辑的翻译σ，翻译分为语法和语义两个部分。给定一个关系数据库d，σ的语义部分将d转化为一个DMDL的标准模型σ(d)，σ的语法部分将d的初始信息转化为DMDL的知识库KB(d)，并将d中由关系代数运算生成的新元组和新关系表示为DMDL中的复合元组个体以及动态概念。
3.将关系数据库中各种完整性约束和函数依赖表示为DMDL中的断言，从而将数据库是否满足特定完整性约束或函数依赖归结为DMDL中断言的满足性问题。
4.定义并证明了翻译σ的正确性，从而为关系数据模型的逻辑化表示提供了正确性的保证.σ的正确性包含如下几方面：元组-属性取值断言和元组-关系从属断言的保真，翻译的语义语法两部分的一致性，以及完整性约束和函数依赖断言的保真。
5.给出了DMDL的一组推理规则，包括：关于复合元组和动态概念的引入和消去的推理规则，关于函数依赖的推理规则和关于关系代数运算律的推理规则.在此基础之上，我们给出了这些推理规则的可靠性证明。