Equality and Domain Closure in First-Order Databases

Abstract

A class of first-order databases with no function signs is considered. A closed database DB is one for which the only existing individuals are those explicitly referred to in the formulas of DB. Formally, this is expressed by including in DB a domain closure axiom ( x ) x = c ₁ ∨···∨ x = c _p , where c ₁ ,…, c _p are all of the constants occurring in DB. It is shown how to completely capture the effects of this axiom by means of suitable generalizations of the projection and division operators of relational algebra, thereby permitting the underlying theorem prover used for query evaluation to ignore this axiom. A database is E-saturated if all of its constants denote distinct individuals. It is shown that such databases circumvent the usual problems associated with equality, which arise in more general databases. Finally, it is proved for Horn databases and positive queries that only definite answers are obtained, and for databases with infinitely many constants that infinitely long indefinite answers can arise.