Proving the Equivalence of CLP Programs

摘要

This paper presents two proof systems for the equivalence of programs. The language concerned is CLP to which the universal quantifier is added (CLPany). Both systems axe 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.