May 8, 2012
Pablo Chico de Guzmán
The evaluation of Prolog, the most successful Logic Programming language, is based on the SLD resolution strategy. SLD performs depth-first search and it is efficient in memory, but it can enter infinite loops even when there is a logical derivation for a Prolog query/program. Tabling attacks this declarativeness issue, ensuring termination of programs with the bounded term-size property by using a fixpoint procedure. We give an intuition how tabling execution proceeds, which is an evolution of memoization. As memoization, tabling can also improve the efficiency of programs which repeat computations and can be used to evaluate programs with stratified negation.
Constraint LP (CLP) is a natural extension of LP which attracts much attention. CLP systems apply constraint solving techniques which blend seamlessly with the characteristics of logical variables. Obviously, CLP systems can also benefit from the power of tabling in order to improve their declarativeness and (in many cases) also their efficiency. But existing solutions for the combination of tabling and CLP (TCLP) are unsatisfactory.
We present a complete implementation framework for TCLP, independent from the constraint solver. The constraint solver must provide entailment and projection operation for the tabling engine. We have successfully applied this framework to solve Timed Automata problems by combining tabling evaluation with difference constraints. Our TCLP framework offers fixpoint computations parametrized by constraint domains and it is embedded in a general purpose programming language (Prolog) with promising performance results.