Peng Fu, Ekaterina Komendantskaya: Operational semantics of resolution and productivity in Horn clause logic. Formal Aspects Comput. 29(3): 453-474 (2017)