A FRAMEWORK TO INCORPORATE NONMONOTONIC REASONING INTO CONSTRAINT LOGIC PROGRAMMING

Impressive work has been done in the last years concerning the meaning of negation and disjunction in logic programs, but most of this resea rch concentrated on propositional programs only. While it suffices to consider the propositional case for investigating general properties a nd the overall behavior of a semantics, we feel that for real applicat ions and for computational purposes an implementation should be able t o handle first-order programs without grounding them. In this paper we present a theoretical framework by defining a calculus of program tra nsformations that apply directly to rules with variables and function symbols. Our main results are that (a) this calculus is weakly conflue nt for arbitrary programs (ie., it has the normal form property), (b) it is weakly terminating for Datalog(V,inverted left perpendicular) pr ograms, (c) for finite ground programs it is equivalent to a weakly te rminating calculus introduced by Brass and Dix (1995), and (d) it appr oximates a generalization of Disjunctive Well-founded semantics (D-WFS ) for arbitrary programs. We achieve this by transforming program rule s 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 constra int theory known from CLP can be exploited in the context of non-monot onic reasoning, not only equational constraints over the Herbrand doma in. However, the respective constraint solver must be able to treat ne gative constraints of the considered constraint domain. Tn summary, th is work yields the basis for a general combination of two paradigms: c onstraint logic programming and non-monotonic reasoning. (C) 1995 Else vier Science Inc. All rights reserved.