On Treating Negation within XSB (and upon Extending XSB Programming with a Form of Logical Negation, and its Relations to Existing Varieties of Logic Programming)

Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning

Volume

Papers from the 2001 AAAI Spring Symposium

Contents

A variety of techniques within logic programming have developed for treating negated formulae. These essentially involve constructibility restrictions which are imposed upon complexity classes of quantifieational formulae, and which thereby determine models and model classes of computer programs declaratively regarded. These construetibility restrictions are themselves implemented by imposing restrictions upon both the syntax and semantics of particular computing languages such as Prolog. Current alternative paradigms of logic programming in Prolog include the theorem-proving implementing semantics of first-order conjunctive normal form assertions, and definite and Horn clause logic programming systems. In this paper we discuss some relationships between the resolution principle and these systems, particularly as they concern implementations of negation -- from negation-asfailure through the treatment of negation within the Prolog extension XSB, involving tabling. We examine another proposal [T. Van Le, 1993] for the treatment of negation in Prolog, and we produce an interim report on implementing this form of negation within XSB, including a formal characterization, timing results, and comments upon heuristics. We also provide examples of the use of negation in XSB on knowledge based reasoning applications., and discuss practical performance issues as well as implications for knowledge engineering that follow from implementing this facility.