Lifted Relational Algebra with Recursion and Connections to Modal Logic

TL;DR

This paper introduces a lifted relational algebra with recursion and information propagation, connecting it to modal logic and enabling advanced reasoning about heterogeneous data and decision procedures.

Contribution

It extends Codd's relational algebra to classes of structures with recursion and information flow, linking it to modal logic and enhancing reasoning capabilities.

Findings

Establishes a connection between query evaluation and temporal logic model checking.

Reveals a correspondence between classical and modal logics.

Provides a formal framework for reasoning about heterogeneous information and decision procedures.

Abstract

We propose a new formalism for specifying and reasoning about problems that involve heterogeneous "pieces of information" -- large collections of data, decision procedures of any kind and complexity and connections between them. The essence of our proposal is to lift Codd's relational algebra from operations on relational tables to operations on classes of structures (with recursion), and to add a direction of information propagation. We observe the presence of information propagation in several formalisms for efficient reasoning and use it to express unary negation and operations used in graph databases. We carefully analyze several reasoning tasks and establish a precise connection between a generalized query evaluation and temporal logic model checking. Our development allows us to reveal a general correspondence between classical and modal logics and may shed a new light on the good computational properties of modal logics and related formalisms.