1. 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.
  2. K. R. Apt (1997): From logic programming to Prolog. Prentice Hall.
  3. 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.
  4. 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.
  5. K. Doets (1993): Levationis laus. J. Logic and Computation 3(5), pp. 487–516, doi:10.1093/logcom/3.5.487.
  6. E. Eder (1985): Properties of substitutions and unifications. J. Symbolic Computation 1(1), pp. 31–46, doi:10.1016/S0747-7171(85)80027-4.
  7. J. Gallier (2015): Logic for computer science: Foundations of automatic theorem proving, 2. edition. Dover.
  8. 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.
  9. 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.
  10. 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.
  11. J. W. Lloyd (1987): Foundations of logic programming, 2. edition. Springer-Verlag, doi:10.1007/978-3-642-83189-8.
  12. 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.
  13. C. Palamidessi (1990): Algebraic properties of idempotent substitutions. In: Proc. 17th ICALP, LNCS 443. Springer-Verlag, pp. 386–399, doi:10.1007/BFb0032046.
  14. G. D. Plotkin (1971): Automatic methods of inductive inference. U. of Edinburgh. Available at
  15. 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.
  16. 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.
  17. 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

Comments and questions to:
For website issues: