Reasoning about embedded dependencies using inclusion dependencies

TL;DR

This paper introduces a complete axiomatization for reasoning about embedded dependencies using the chase algorithm, inclusion dependencies, and implicit existential quantification, addressing the undecidability of the implication problem.

Contribution

It presents a novel proof system that extends the chase algorithm with inclusion dependencies and existential quantification for embedded dependencies.

Findings

Provides a complete axiomatization for embedded dependencies.

Demonstrates the effectiveness of the chase-based proof system.

Addresses the undecidability issue with a constructive proof method.

Abstract

The implication problem for the class of embedded dependencies is undecidable. However, this does not imply lackness of a proof procedure as exemplified by the chase algorithm. In this paper we present a complete axiomatization of embedded dependencies that is based on the chase and uses inclusion dependencies and implicit existential quantification in the intermediate steps of deductions.