A Predicate Transformer for Unification.
Livio Colussi, Elena Marchiori · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1992
In this paper we study unification as predicate transformer.Given a unification problem expressed as a set of sets of terms U and a predicate P, we are interested in the strongest predicate R (w.r.t. the implication) s.t.if P holds before the unification of U then R holds when the unification is performed.We introduce a Dijkstra-style calculus that given P and U computes R. We prove the soundness, completeness and termination of the calculus.The predicate language considered contains monotonic predicates together with some nonmonotonic predicates like var, -,ground, share and -,share.This allows to use the calculus for the static analysis of run-time properties of Prolog programs.