An extended constraint deductive database: Theory and implementation

•The basis logic extends Horn clauses with implications and universal quantifiers.•We present a proof semantics and a fixpoint semantics, which are equivalent.•We describe a constraint deductive database system based on the fixpoint semantics.•We provide three domain instances which support aggregate functions.

The scheme of Hereditary Harrop formulas with constraints, HH(C), has been proposed as a basis for constraint logic programming languages. In the same way that Datalog emerges from logic programming as a deductive database language, such formulas can support a very expressive framework for constraint deductive databases, allowing hypothetical queries and universal quantifications. As negation is needed in the database field, HH(C) is extended with negation to get HH¬(C). This work presents the theoretical foundations of HH¬(C) and an implementation that shows the viability and expressive power of the proposal. Moreover, the language is designed in a flexible way in order to support different constraint domains. The implementation includes several domain instances, and it also supports aggregates as usual in database languages. The formal semantics of the language is defined by a proof-theoretic calculus, and for the operational mechanism we use a stratified fixpoint semantics, which is proved to be sound and complete w.r.t. the former. Hypothetical queries and aggregates require a more involved stratification than the common one used in Datalog. The resulting fixpoint semantics constitutes a suitable foundation for the system implementation.