CLP Entailment as Lazy Clause Generation
Gregory Duck and Joxan Jaffar
Abstract
In this paper we present an algorithm for deciding entailment G |= H
of properties G and H defined using Constraint Logic Programming
(CLP). The algo rithm is based on Satisfiability Modulo Theories (SMT)
over a theory derived from the C LP program. The im- plementation is
based on lazy clause generation. Existing methods f or discharging
such entailments rely on applying a set of proof rules (such as
unfoldin g, constraint solving, and induction) as part of a naive
search. Our contribution is to use a SAT solver for the search, and
thus enjoy benefits this bestows, such as efficie nt back-jumping,
no-good learning, unit propagation, etc.