An approach to proving properties of non-terminating logic programs