Discovery of equational replacement proofs using the congruence closure

摘要

Given a set of equalities and two terms a and b, the problem to solve is to find a proof of a = b. This is usually done basically in the form of an "equa lity chain" a = c/sub 1/ = c/sub 2/ = ... = c/sub n/ = b. This kind of proof is indeed very easy to understand and explain once it has been discovered, but this discovery is itself fairly difficult. In this work we describe a completely deterministic and mechanical method for discovering this kind of proofs, using on a forward chaining method based on the Congruence Closure.