This paper introduces a logic for a class of properties - in particular variable aliasing - used in static analysis of logic programs. The logic is shown to be sound, complete and decidable. Moreover, it is illustrated how this logic can be applied to automatize some parts of the reasoning when proving the partial correctness of a logic program.