A Theoretical Study of (Full) Tabled Constraint Logic Programming

TL;DR

This paper provides a comprehensive theoretical analysis of full Tabled Constraint Logic Programming (TCLP), focusing on semantics, correctness, termination, and implementation aspects within the Ciao Prolog system.

Contribution

It introduces a top-down semantics for TCLP, analyzes how constraints affect termination, and evaluates the impact of constraint projection variants on correctness and completeness.

Findings

Top-down semantics for TCLP is equivalent to fixpoint semantics.

Constraints significantly influence termination behavior.

Different constraint projection methods affect TCLP correctness and completeness.

Abstract

Logic programming with tabling and constraints (TCLP, tabled constraint logic programming) has been shown to be more expressive and, in some cases, more efficient than LP, CLP, or LP with tabling. In this paper we provide insights regarding the semantics, correctness, completeness, and termination of top-down execution strategies for full TCLP, i.e., TCLP featuring entailment checking in the calls and in the answers. We present a top-down semantics for TCLP and show that it is equivalent to a fixpoint semantics. We study how the constraints that a program generates can effectively impact termination, even for constraint classes that are not constraint compact, generalizing previous results. We also present how different variants of constraint projection impact the correctness and completeness of TCLP implementations. All of the presented characteristics are implemented (or can be experimented with) in Mod TCLP, a modular framework for Tabled Constraint Logic Programming, part of the Ciao Prolog logic programming system.