Constraint Logic Programming has been successful as a programming language, and more recently, as a model of executable specifications. There have been numerous works which use CLP to model programs and which use an adaptation of the CLP proof system for proving certain properties, for example, the XMC system [3] uses SLG resolution on alternation-free μ-calculus formulas, and the work on deductive model checking [1] model for CTL properties on transition systems represented as CLP rules. These, amongst other works, cover a limited class of programs and use specialized proof methods. In our work, we present a systematic method to model a general class of programs, and provide adaptations of the CLP proof systems in order to provide a systematic and general proof method.