Constraint Logic Programming in the Sequent Calculus

Abstract In this paper, we are developing a new logical semantics of CLP. It is shown that CLP is based on an amalgamated logic embedding the entailment relation of constraints into a fragment of intuitionistic logic. Constrained SLD resolution corresponds to a complete proof search in the amalgamated logic. The framework provides not only the logical account on the definitional semantics towards CLP but also a general way to integrate constraints into various logic programming systems.

Authors

• John Darlington
• Yike Guo

Keywords

No keywords are indexed for this paper.