Fages, François Constructive negation by pruning. (English) Zbl 0882.68034 J. Log. Program. 32, No. 2, 85-118 (1997). Summary: We 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. Cited in 7 Documents MSC: 68N17 Logic programming Keywords:pruning mechanism; constructive negation by pruning; constraint logic programs PDFBibTeX XMLCite \textit{F. Fages}, J. Log. Program. 32, No. 2, 85--118 (1997; Zbl 0882.68034) Full Text: DOI