## 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?