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?

About these ads

2 Responses to “A long long proof”

  1. J S Says:

    Which prover are you using?


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: