ILP Modulo Data

TL;DR

This paper introduces a new decidable logic combining linear integer arithmetic with relational algebra operators, enabling scalable automated reasoning over data for analysis and decision-making.

Contribution

It presents a novel logic extending quantifier-free linear integer arithmetic with relational algebra, along with a scalable decision procedure based on BC(T) architecture.

Findings

Decision procedure is scalable and efficient.

Experimental evaluation demonstrates practical applicability.

Potential for enhanced data analysis tools.

Abstract

The vast quantity of data generated and captured every day has led to a pressing need for tools and processes to organize, analyze and interrelate this data. Automated reasoning and optimization tools with inherent support for data could enable advancements in a variety of contexts, from data-backed decision making to data-intensive scientific research. To this end, we introduce a decidable logic aimed at database analysis. Our logic extends quantifier-free Linear Integer Arithmetic with operators from Relational Algebra, like selection and cross product. We provide a scalable decision procedure that is based on the BC(T) architecture for ILP Modulo Theories. Our decision procedure makes use of database techniques. We also experimentally evaluate our approach, and discuss potential applications.