Krafft, Dean B.Demers, Alan J.2007-04-232007-04-231981-04http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR81-458https://hdl.handle.net/1813/6298Several existing program verification and automated prooff systems make use of similar decision procedures for equality ([Krafft 1978], [Nelson and Oppen 1977] and [Downey, Sethi and Tarjan 1980]). The general method used by these algorithms has been named congruence closure. Given two expressions on uninterpreted function symbols, a congruence closure algorithm determines whether the expressions can be deduced to be equal from a set of previously asserted equalities. The existing congruence closure algorithms do not provide any indication of which previously asserted equalities were required in the deduction. In this paper, we describe an extension to one version of congruence closure. When two expressions are equal, the new algorithm can provide a certificate of their equality: a list of prevviously asserted equalities from which the queried equality can be deduced. This list is minimal, in the sense that if any equality iss removed from the list, the queried equality can no longer be deduced. The running time to produce the certificate is almost-linear in the size of the list.2872185 bytes798097 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report