In [Wastl 1998] we have introduced the Hilbert style inference system K for deriving all keys of a database relation schema. In this paper we investigate formal K-derivations more closely using the concept of tableaux. The analysis gives insight into the process of deriving keys of a relation schema. Also, the concept of tableaux gives a proof procedure for computing all keys of a relation schema. In practice, the methods developed here will be usefull for computing keys or for deciding whether an attribute is a key attribute, respectively non-key attribute. This decision problem becomes relevant when checking whether a relation schema is in third normal form, or when applying the well-known 3NF-decomposition algorithm (a.k.a. 3NF-synthesis algorithm).

database relation schema, keys, automated deduction