Example proofs demonstrating Casanova et al ’s axiom system for IND:

• IND1 Reflexivity: if X Í schema(R) with R < R, then I |– R[X] Í R[X].

 if X Í schema(R) with R ∈R, then I |- R[X] Í R[X]

Example:

{branch-name} Í Branch-schema

I|- Branch-schema[branch-name] Í  Branch-schema[branch-name] by IND1

 

• IND2 Projection and permutation:

if I |– R₁[X] Í R₂[Y], then I |– R₁[X₁] Í R₁[Y₁], where X₁ and Y₁ are the projection and permutation on X and Y, respectively.

Example:

 Let r₁ and r₂ be two relations over Loan-schema and Borrower-schema. Consider the resulting relation of the join, r₁ |><| r₂ over the relation schema S = Loan-schema U Borrower-schema.

The following inclusion dependency is satisfied.

I|-S[loan-number, branch-name] Í Loan-schema[loan-number, branch-name]

We can derive new inclusion dependencies by IND2 as follows:

I|-S[branch-name, loan-number] Í Loan-schema[branch-name, loan-number] by IND2

And

I|-S[loan-number] Í Loan-schema[loan-number] by IND2

 

• IND3 Transitivity:

if I |– R₁[X] Í R₂[Y] and I |– R₂[Y] Í R₃[Z], then I |– R₁[X] Í R₃[Z].

Example:

I |– Customer-credit-card-schema[customer-id] Í Account-schema[customer-id]

And

I |– Account-schema[customer-id] Í Customer-schema[customer-id]

We can derive the following new inclusion dependency by IND3 as follows:

I |– Customer-credit-card-schema[customer-id] Í Customer-schema[customer-id]

by IND3