Syllabus
Relation between SLD-resolution and pure Prolog. Domains, data structures.
Termination of Prolog programs, staged mappings. Occur-check, modes of programs, linear terms. Partial correctness, pre- and post-conditions.
Negative information. Nonmonotonic deduction, closed world assumption, deduction rule "negation by failure". Characterization of finite failure.
Completion of logic program. Transformation from logic program P with negation to its completion, programs IF(P), IFF(P) and completion. Correctness of the rule
"negation by failure". Completeness of the rule "negation by failure".
Annotation
Prolog and its procedures, domains, data structures. Semantics of logic programs, Termination,
Occur-check. Partial correctness, pre- and post-conditions. Negative information, rule "Negation by failure", nonmonotonic reasoning.