This paper presents two proof systems for the equivalence of programs. The language concerned is CLP to which the universal quantifier is added (CLP∀). Both systems are based on first order classical logic.
The first uses an induction rule and allows one to prove that the set of finite successes of a program is included in another program’s corresponding set. The second uses a coinduction rule for proving the inclusion of the sets of infinite successes which contain the finite successes.
Finally we show that the proof systems are equivalent under some natural conditions.