Armstrong 公理系统

Armstrong 公理系统（Armstrong Axiom System）是一套用于函数依赖（FD）的推理规则 [1]。它是数据库模式分解算法的理论基础，并被认为是有效且完备的公理系统 [1]。

该系统包括以下三条基本推理规则：

1. 自反律 (Reflexivity)：如果属性集 Y 是属性集 X 的子集（Y ⊆ X），那么 X 函数地决定 Y (X → Y) [1]。
2. 增广律 (Augmentation)：如果 X 函数地决定 Y (X → Y)，并且 Z 是任意属性集，那么 XZ 函数地决定 YZ (XZ → YZ) [1]。
3. 传递律 (Transitivity)：如果 X 函数地决定 Y (X → Y)，并且 Y 函数地决定 Z (Y → Z)，那么 X 函数地决定 Z (X → Z) [1]。

根据这三条基本规则，还可以推导出其他推理规则，例如 [1]：

• 合并规则：由 X → Y 和 X → Z，可以得到 X → YZ。
• 伪传递规则：由 X → Y 和 WY → Z，可以得到 XW → Z。
• 分解规则：由 X → Y 和 Z ⊆ Y，可以得到 X → Z。

有效性与完备性是 Armstrong 公理系统的两个重要特性 [1]：

• 有效性：任何由给定函数依赖集 F 根据 Armstrong 公理推导出来的函数依赖，一定被 F 逻辑蕴含（即属于 F 的闭包 F+）[1]。
• 完备性：F+ 中的每一个函数依赖，必定可以由给定函数依赖集 F 根据 Armstrong 公理推导出来 [1]。

Armstrong 公理系统为判断一个函数依赖是否被其他函数依赖逻辑蕴含提供了方法，这对于关系模式的规范化和数据库设计至关重要 [1]。