Proving properties of Logic Programs by Abstract Diagnosis