by Michael Codish, Dennis Dams, and Eyal Yardeni.
In Koichi Furukawa, editor, Logic Programming. Proceedings of the Eighth International Conference Logic Programming, pages 79-93, The MIT Press, Cambridge, Mass., 1991.
We derive and prove safe an abstract unification algorithm for groundness and sharing analysis in logic programs. In general, proving the safety of abstract unification plays a crucial role in the construction of an abstract interpretation. We adopt a notion of abstract substitutions which is originally due to Søndergaard and derive an abstract unification algorithm by abstracting the process of unifying a pair of concrete atoms. This results in a concise and well motivated definition of abstract unification together with a proof of its safety. The resulting algorithm appears to formally reconstruct that intended by Søndergaard. The approach followed in deriving the algorithm is interesting in its own; to appreciate its advantages it is sufficient to compare our presentation of the algorithm with previous ones, and to note that those previous are not accompanied by proofs of safety.