A long long proof
May 7, 2012
Decomposition of a relation into join of projections serves as motivation for database normalization theory. In relational lattice terms relation
x projected into sets of attributes (that is empty relations)
x = (x v s) ^ (x v t)
Lets investigate dual perspective and switch the roles of join and inner union:
x = (x ^ s) v (x ^ t)
One particular instance of this identity is known as fundamental decomposition identity
x = (x ^ R00) v (x ^ R11)
which informally asserts that a relation is an inner union of the relation header (i.e. set of attributes) and content (set of tuples). Fundamental decomposition identity can be generalized into
x = (x ^ y`) v (x ^ y')
' is relation complement and
` is attribute inversion. Both operations are domain dependent (which might explain a reluctance of some researchers adopting them). Automated proof of generalized decomposition identity
% Language Options op(300, postfix, "`" ). formulas(assumptions). % Standard lattice axioms x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v y = y v x. (x v y) v z = x v (y v z). x v (x ^ y) = x. % Litak et.al. x ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))). (x ^ y) v (x ^ z) = x ^ ( ((x v z) ^ y) v ((x v y) ^ z) ). (R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y). % Unary postfix negation operation ' aka <NOT> x' ^ x = x ^ R00. x' v x = x v R11. % Unary postfix inversion operation ` aka <INV> x` ^ x = R11 ^ x. x` v x = R00 v x. % FDI x = (x ^ R00) v (x ^ R11). % Distributivity of join over outer union aka <OR> x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'. end_of_list. formulas(goals). x = (x ^ y') v (x ^ y`). end_of_list.
turned out to be quite CPU consuming
% -------- Comments from original proof --------
% Proof 1 at 4894.53 (+ 50.37) seconds.
% Length of proof is 867.
% Level of proof is 47.
% Maximum clause weight is 61.
% Given clauses 10875.
How fast is your system?