CLP(CHI) FOR AUTOMATICALLY PROVING PROGRAM PROPERTIES

Various proof methods have been proposed to solve the implication prob lem, i.e. proving that properties of the form: For All(P --> Q) - wher e P and Q denote conjunctions of atoms - are logical consequences of l ogic programs. Nonetheless, it is commonplace to say that it is still quite a difficult problem. Besides, the advent of the constraint logic programming scheme constitutes not only a major step towards the achi evement of efficient declarative logic programming systems but also a new held to explore. By recasting and simplifying the implication prob lem in the constraint logic programming (CLP) framework, we define a g eneric proof method for the implication problem, which we prove sound from the algebraic point of view. We present four examples using CLP(N ), CLP(RT), CLP(Sigma) and RISC-CLP(R). The logical point of view of the constraint logic programming scheme enables the automation of the proof method. At last, we prove the unsolvability of the implication p roblem, we point out the origins of the incompleteness of the proposed proof method and we identify two classes of programs for which we giv e a decision procedure for the implication problem. (C) 1998 Elsevier Science Inc. All rights reserved.