## 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) `s`

and `t`

:

`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')`

where the `'`

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?

May 12, 2012 at 1:13 pm

Which prover are you using?

May 13, 2012 at 10:28 pm

Prover9