On Graph Refutation for Relational Inclusions

TL;DR

This paper presents a new graphical refutation calculus for relational inclusions that simplifies the process of proving such inclusions by reducing it to checking graph emptiness, making it more accessible and easier to use.

Contribution

It introduces a sound and complete graphical calculus for relational inclusions, offering a simpler and more user-friendly alternative to traditional methods.

Findings

The calculus is sound and complete.

It reduces relational inclusion proofs to graph emptiness checks.

The method is conceptually simpler than existing approaches.

Abstract

We introduce a graphical refutation calculus for relational inclusions: it reduces establishing a relational inclusion to establishing that a graph constructed from it has empty extension. This sound and complete calculus is conceptually simpler and easier to use than the usual ones.