|
|
|
||
|
Horn logic, logic programs, procedural interpretation
of logic programs,
Prolog and its procedures, semantics of
logic programs, Termination,
Occur-check
Last update: T_KTI (12.05.2004)
|
|
||
|
To learn theory and techniques used in logic programming. Last update: Hric Jan, RNDr. (07.06.2019)
|
|
||
|
Oral exam on topics from lecture. Last update: Hric Jan, RNDr. (07.06.2019)
|
|
||
|
Krzysztof R. Apt: From Logic Programming to Prolog, Prentice Hall International Series in Computer Science, 1996, ISBN-13: 978-0132303682
Krzysztof R. Apt , Roland Bol: Logic Programming and Negation: A survey. Journal of Logic Programming, 1994, vol. 19, pp. 9-71
John W. Lloyd. Foundations of Logic Programming (2nd edition). Springer-Verlag 1987 Last update: T_KTI (14.05.2013)
|
|
||
|
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.
Last update: T_KTI (14.05.2015)
|