Second-Order Specifications and Quantifier Elimination for Consistent Query Answering in Databases

TL;DR

This paper explores how to use second-order logic and quantifier elimination to efficiently compute consistent answers to queries in databases with inconsistencies, transforming repair-based reasoning into logical inference.

Contribution

It introduces a method to convert repair programs into second-order logic theories and applies quantifier elimination to obtain first-order theories for consistent query answering.

Findings

Repairs can be represented as stable models of disjunctive logic programs.

Second-order logic can specify database repairs and consistent answers.

Quantifier elimination yields first-order theories for efficient reasoning.

Abstract

Consistent answers to a query from a possibly inconsistent database are answers that are simultaneously retrieved from every possible repair of the database. Repairs are consistent instances that minimally differ from the original inconsistent instance. It has been shown before that database repairs can be specified as the stable models of a disjunctive logic program. In this paper we show how to use the repair programs to transform the problem of consistent query answering into a problem of reasoning w.r.t. a theory written in second-order predicate logic. It also investigated how a first-order theory can be obtained instead by applying second-order quantifier elimination techniques.