G. Amato & F. Scozzari (2009):
Optimality in goal-dependent analysis of sharing.
Theory and Practice of Logic Programming 9(5),
pp. 617–689,
doi:10.1017/S1471068409990111.
K. R. Apt (1997):
From logic programming to Prolog.
Prentice Hall.
K. R. Apt & M. H. van Emden (1982):
Contributions to the theory of logic programming.
J. of ACM 29(3),
pp. 841–862,
doi:10.1145/322326.322339.
R. N. Bol (1992):
Generalizing completeness results for loop checks in logic programming.
Theor. Comp. Sci. 104(1),
pp. 3–28,
doi:10.1016/0304-3975(92)90164-B.
K. Doets (1993):
Levationis laus.
J. Logic and Computation 3(5),
pp. 487–516,
doi:10.1093/logcom/3.5.487.
E. Eder (1985):
Properties of substitutions and unifications.
J. Symbolic Computation 1(1),
pp. 31–46,
doi:10.1016/S0747-7171(85)80027-4.
J. Gallier (2015):
Logic for computer science: Foundations of automatic theorem proving,
2. edition.
Dover.
D. Jacobs & A. Langen (1992):
Static analysis of logic programs for independent AND parallelism.
J. of Logic Programming 13(2-3),
pp. 291 – 314,
doi:10.1016/0743-1066(92)90034-Z.
M. Kulaš (2005):
Toward the concept of backtracking computation.
In: L. Aceto, W. J. Fokkink & I. Ulidowski: Proc. of the Workshop on Structural Operational Semantics (SOS'04), London,
ENTCS 128.
Elsevier,
pp. 39–59,
doi:10.1016/j.entcs.2004.10.026.
J. L. Lassez, M. J. Maher & K. Marriott (1988):
Unification revisited.
In: M. Boscarol, L. Carlucci Aiello & G. Levi: Foundations of Logic and Functional Programming,
LNCS 306.
Springer Berlin Heidelberg,
pp. 67–113,
doi:10.1007/3-540-19129-1_4.
J. W. Lloyd (1987):
Foundations of logic programming,
2. edition.
Springer-Verlag,
doi:10.1007/978-3-642-83189-8.
J. W. Lloyd & J. C. Shepherdson (1991):
Partial evaluation in logic programming.
J. of Logic Programming 11(3-4),
pp. 217–242,
doi:10.1016/0743-1066(91)90027-M.
C. Palamidessi (1990):
Algebraic properties of idempotent substitutions.
In: Proc. 17th ICALP,
LNCS 443.
Springer-Verlag,
pp. 386–399,
doi:10.1007/BFb0032046.
C. Pusch (1996):
Verification of compiler correctness for the WAM.
In: Proc. TPHOLs,
LNCS 1125.
Springer Berlin Heidelberg,
pp. 347–361,
doi:10.1007/BFb0105415.
J. C. Shepherdson (1994):
The role of standardising apart in logic programming.
Theor. Comp. Sci. 129(1),
pp. 143–166,
doi:10.1016/0304-3975(94)90084-1.
C. Urban, A. Pitts & M. Gabbay (2004):
Nominal unification.
Theoretical Computer Science 323(1-3),
pp. 473–497,
doi:10.1016/j.tcs.2004.06.016.
Proof on http://www.inf.kcl.ac.uk/staff/urbanc/Unification/..