阿姆斯特朗公理系统（）是一组用于推导关系数据库中所有函数依赖的规则。这一系统由威廉·W·阿姆斯特朗在1974年的论文中首次提出。当应用于函数依赖集（用 F 表示）时，这些规则在生成该集闭包（用 F^{+} 表示）中的函数依赖方面既可靠又完备。换言之，反复应用这些规则，我们能够推导出闭包 F^+ 中的所有函数依赖，且不会产生不属于该闭包的依赖关系。
让我们用更严谨的方式来描述这个概念。假设 \langle R(U), F \rangle 代表一个关系模式，其中 U 是属性集，F 是函数依赖集。如果所有满足 F 中函数依赖的，R 的实例 r，也都同时满足函数依赖 f，那么我们就说 f 被 F 逻辑蕴含，记作 F \models f。我们用 F^{+} 来表示所有被 F 逻辑蕴含的函数依赖的集合。
再来看推理规则集 A 的作用。如果我们能够通过反复运用 A 中的规则，从 F 中推导出函数依赖 f，我们就说 f 可由 F 通过 A 所推导，记作 F \vdash _{A} f。我们用 F^{*}_{A} 表示所有可以通过 A 从 F 推导出的函数依赖的集合。
那么，当且仅当以下条件成立时，推理规则集 A 是可靠的：
:
F^{*}_{A} \subseteq F^{+}
也就是说，使用 A 推导出的函数依赖不能超出由 F 逻辑蕴含的函数依赖范围。
推理规则集 A 的完备性当且仅当以下条件成立：
:
F^{+} \subseteq F^{*}_{A}
更简单地说，推理规则集 A 能够推导出所有由 F 逻辑蕴含的函数依赖。
公理（基本规则）
设R(U)是定义在属性集U上的关系模式。在接下来的讨论中，我们将用X、Y、Z表示U的任意子集。为了简洁，我们用XY代替常规的X \cup Y来表示两个属性集X和Y的并集。这种记法在处理資料庫理論中的属性集合时是相当常见的。
自反律
如果X是一个属性集，Y是X的一个子集，那么X函数决定Y（也就是Y函数依赖X），记作X \to Y。
:若Y \subseteq X则X \to Y.
增广律
如果X决定Y，那么在X和Y中同时添加任意属性集Z后，这种决定关系仍然成立。这表明，增加新的属性不会改变已有的函数依赖关系。
:若X \to Y，则对任意属性集Z，都有X Z \to Y Z.
传递律
函数依赖关系具有传递性。也就是说，如果X决定Y，且Y决定Z，那么X必然也决定Z。
:若X \to Y且Y \to Z，则X \to Z.
公理的推论
这些推论可以从上述公理中推导出来。
分解规则
若X \to Y Z，则 X \to Y且 X \to Z。
证明
合成规则
若X \to Y且A \to B，则 X A \to Y B。
证明
合并规则
如果X \to Y且X \to Z，则X \to YZ。
证明
伪传递规则
若X \to Y且 Y Z \to W，则 X Z\to W。
证明
自确定性
对于任意I， I \to I。这直接由自反性公理得到。
扩展规则
当Z=X时，该属性是增广性的一个特殊情况。
:若X \to Y，则X \to X Y。
在这种意义上，扩展性可以替代增广性作为公理，因为通过扩展性和其他公理可以证明增广性。
证明
参考文献
外部链接
- [http://www.cs.umbc.edu/courses/461/current/burt/lectures/lec14/ UMBC CMSC 461 Spring '99]
- [http://www-db.stanford.edu/~ullman/cs345notes/slides01-1.ps CS345 Lecture Notes from Stanford University]
评论 (0)