On the Decidability and Axiomatization of Query Finiteness in Deductive Databases

A database query is finite 1 if its result consists of a finite set of tuples. For queries formulated as sets of pure Horn rules, the problem of determining finiteness is, in general, undecidable. In this paper we consider superfiniteness---a stronger kind of finiteness, which applies to Horn queries whose function symbols are replaced by the abstraction of infinite relations with finiteness constraints (abbr., FC's). We show that superfiniteness is not only decidable but also axiomatizable, and the axiomatization yields an effective decision procedure. Although there are finite queries that are not superfinite, we demonstrate that superfinite queries represent an interesting and nontrivial subclass within the class of all finite queries. Then we turn to the issue of inference of finiteness constraints---an important practical problem that is instrumental in deciding if a query is evaluable by a bottom-up algorithm. Although it is not known whether FC-entailment is decidable for set..