Lars Hallnäs, Peter Schroeder-Heister: A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules. J. Log. Comput. 1(2): 261-283 (1990)