Syllabus
Introduction. Horn logic as fragment of first-order predicate logic, syntax of Horn clauses and logic programs.
Substitution and unification. Unification substitution and unification algorithm. Idempotent and relevant substitutions.
Computation process, SLD-resolution. Resolution step, SLD-derivation and their properties, lemma about variants. Refutation by resolution, SLD-trees.
Semantics of logic programs. Correctness of SLD-resolution, Herbrand models of logic programs, direct consequence operator, operators and fixed-points. Least
Herbrand model and its characterization.
Completeness of SLD-resolution, Substitution lemma, success set of logic program, its relation to least Herbrand model. Theorem about completeness of SLD-resolution.
Answer substitution. Correct answer substitution, strong completeness of
SLD-resolution, characterization of success set of logic program.
Annotation
Horn logic, logic programs, procedural interpretation of logic programs,
Prolog and its procedures, semantics of logic programs, Termination,
Occur-check