Implementing CLP( ) using the Connection Theorem Proving Method and a Clause Management Systems

Constraint Logic Programming (CLP) is an extension of logic programming to include efficient constraint processing algorithms for specialized computational domains. CLP( ) is a CLP language which processes constraints in Boolean algebra. The CLP( ) language can be used to solve many set theoretic and propositional logic problems including digital circuit design, analysis, and verification. This paper formally describes a new way to implement CLP( ) using the connection theorem proving method (CM) and a clause management system (CMS). The CM and a CMS provide a simple and efficient way to implement CLP( ).