A framework to incorporate non-monotonic reasoning into constraint logic programming

AbstractImpressive work has been done in the last years concerning the meaning of negation and disjunction in logic programs, but most of this research concentrated on propositional programs only. While it suffices to consider the propositional case for investigating general properties and the overall behavior of a semantics, we feel that for real applications and for computational purposes an implementation should be able to handle first-order programs without grounding them. In this paper we present a theoretical framework by defining a calculus of program transformations that apply directly to rules with variables and function symbols. Our main results are that (a) this calculus is weakly confluent for arbitrary programs (i.e., it has the normal form property), (b) it is weakly terminating for Datalog ∨,¬ programs, (c) for finite ground programs it is equivalent to a weakly terminating calculus introduced by Brass and Dix (S.Brass, J.Dix, in: J.Dix, L.Pereira, T.Przymusinski (Eds.), Non-monotonic Extensions of Logic Programming, Springer Lecture Notes in Artificial Intelligence, Vol.927, Springer, Berlin, 1995, pp. 127–155), and (d) it approximates a generalization of Disjunctive Well-founded semantics (D-WFS) for arbitrary programs. We achieve this by transforming program rules into rules with equational constraints thereby using heavily methods and techniques from constraint logic programming (CLP). In particular, disconnection-methods play a crucial role. In principle, any constraint theory known from CLP can be exploited in the context of non-monotonic reasoning, not only equational constraints over the Herbrand domain. However, the respective constraint solver must be able to treat negative constraints of the considered constraint domain. In summary, this work yields the basis for a general combination of two paradigms: constraint logic programming and non-monotonic reasoning