Armstrong's axioms are a set of axioms (or, more precisely, inference rules) used to infer all the functional dependencies on a relational database. They were developed by William W. Armstrong on his paper Dependency Structures of Data Base Relationships published in 1974. The axioms are sound in that they generate only functional dependencies in the closure of a set of functional dependencies (denoted as F+) when applied to that set (denoted as F). They are also complete in that repeated application of these rules will generate all functional dependencies in the closure F+. More formally, let <<math>R</math>( <math>U</math>), <math>F</math>> denote a relational scheme over the set of attributes <math>U</math> with a set of functional dependencies <math>F</math>. We say that a functional dependency <math>f</math> is logically implied by <math>F</math>,and denote it with <math>F \models f</math> if and only if for every instance <math>r</math> of <math>R</math> that satisfies the functional dependencies in <math>F</math>, r also satisfies <math>f</math>. We denote by <math>F^{+}</math> the set of all functional dependencies that are logically implied by F. Furthermore, with respect to a set of inference rules <math>A</math>, we say that a functional dependency <math>f</math> is derivable from the functional dependencies in <math>F</math> by the set of inference rules <math>A</math>, and we denote it by <math>F \vdash _{A} f</math> if and only if <math>f</math> is obtainable by means of repeatedly applying the inference rules in <math>A</math> to functional dependencies in <math>F</math>. We denote by <math>F^{*}_{A}</math> the set of all functional dependencies that are derivable from <math>F</math> by inference rules in <math>A</math>. Then, a set of inference rules <math>A</math> is sound if and only if the following holds: <math> F^{+}_{A} \subseteq F^{*} </math> that is to say, we cannot derive by means of <math>A</math> functional dependencies that are not logically implied by <math>F</math>. The set of inference rules <math>A</math> is said to be complete if the following holds: <math> F^{*} \subseteq F^{+}_{A} </math> more simply put, we are able to derive all the functional dependencies that are logically implied by <math>F</math>.
Contents |
Axioms
Let <math>R</math>(<math>U</math>) be a primitive relation scheme over the set of attributes <math>U</math>. Henceforth we will denote by letters <math>X</math>, <math>Y</math>, <math>Z</math> any subset of <math>U</math> and, for short, the union of two sets of attributes <math>X</math> and <math>Y</math> by <math>XY</math> instead of the usual <math>X \cup Y</math>
Axiom of reflexivity
If <math>Y \subseteq X </math>, then <math>X \to Y</math>
Axiom of augmentation
If <math>X \to Y</math>, then <math>XZ \to YZ</math> for any <math>Z</math>
Axiom of transitivity
If <math>X \to Y</math> and <math>Y \to Z</math> , then <math>X \to Z</math>
Additional rules
Union
If <math>X \to Y</math> and <math>X \to Z</math> then <math>X \to YZ</math>
Decomposition
If <math>X \to YZ</math>, then <math>X \to Y</math> and <math>X \to Z</math>
Pseudo Transitivity
If <math>A \to B</math> and <math> CB \to D</math> then <math> AC \to D</math>
