There are rules through which we can deduce that a set of functional dependencies logically implies some other functional dependencies. This deduction is done through “inference rules”. Before we are allowed to use such rules we must prove that they are correct. We must do this by using the definition of what functional dependencies are.
Example: augmentation:
for simplicity we write r R to indicate that an instance r is a valid instance for scheme R. We write t r to indicate that t is a tuple of r. We write X R to indicate that X is a subset of the set of attributes of R. We write XY to mean X Y.
The first proof (augmentation) goes as follows:
(r R, t1, t2 r : t1[X]=t2[X] : t1[Y]=t2[Y]) (this is the definition of X Y)
(r R, t1, t2 r : t1[Z]=t2[Z] : t1[Z]=t2[Z]) (this is always true)
(because ((A B) (C D) (A C) (B D))
(r R, t1, t2 r : t1[X]=t2[X] t1[Z]=t2[Z] : t1[Y]=t2[Y] t1[Z]=t2[Z])
(because a function t[X Z] = t[X] t[Z])
(r R, t1, t2 r : t1[XZ]=t2[XZ] : t1[YZ]=t2[YZ])
(this is the definition of XZ YZ)