Constructive negation by pruning

AbstractWe show that a simple concurrent pruning mechanism over standard SLD derivation trees, called constructive negation by pruning, provides a complete operational semantics for normal constraint logic programs (CLP) w.r.t. Fitting-Kunen's three-valued logic semantics. The principle of concurrent pruning is the only extra machinery needed to handle negation; in particular, there is no need for considering complex subgoals with explicit quantifiers outside the constraint part.The main result of the paper is the definition of a fixpoint semantics for normal CLP programs which is fully abstract for the observation of computed answer constraints. This allows to generalize the s-semantics approach to normal CLP programs, and provides a fixpoint characterization of Kunen's semantics. The definition is based on a nonground continuous finitary version of Fitting's operator.We relate also these results to an important aspect of CLP programming practice: optimization. We investigate various forms of goal optimization within CLP languages, and provide both declarative and operational semantics for them via a translation to normal CLP programs. We show that constructive negation by pruning specializes for these classes of programs to a more efficient concurrent branch and bound like procedure