Simple improvements of a simple solution for inverting resolution

In this paper we address some simple improvements of the algorithm of Rouveirol and Puget [1989] for inverting resolution. Their approach is based on automatic change of representation called flattening and unflattening of clauses in a logic program. This enables a simple implementation of operators, such as Absorption, presented in Muggleton and Buntine [1988]. Unfortunately both the algorithms of MB and RP are incomplete. We analyze the reasons of the incompleteness of the RP algorithm and present an improved Absorption operator. It appears that flat tree epresentations of clauses and predicate calculus with equality provide an appropriate context for these matters.