מיכאל קודיש

We derive and prove safe an abstract unification algorithm for groundness and aliasing 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 Sondergaard 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 Sondergaard. 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.