SubjectsSubjects(version: 875)
Course, academic year 2020/2021
Logic Programming 1 - NAIL076
Title: Logické programování 1
Guaranteed by: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Faculty: Faculty of Mathematics and Physics
Actual: from 2020
Semester: winter
E-Credits: 3
Hours per week, examination: winter s.:2/0 Ex [hours/week]
Capacity: unlimited
Min. number of students: unlimited
State of the course: taught
Language: Czech
Teaching methods: full-time
Guarantor: doc. Mgr. Petr Gregor, Ph.D.
RNDr. Jan Hric
Class: Informatika Mgr. - Teoretická informatika
Informatika Mgr. - Diskrétní modely a algoritmy
Classification: Informatics > Programming, Theoretical Computer Science
K//Is co-requisite for: NAIL077
Annotation -
Last update: T_KTI (12.05.2004)
Horn logic, logic programs, procedural interpretation of logic programs, Prolog and its procedures, semantics of logic programs, Termination, Occur-check
Aim of the course -
Last update: RNDr. Jan Hric (07.06.2019)

To learn theory and techniques used in logic programming.

Course completion requirements -
Last update: RNDr. Jan Hric (07.06.2019)

Oral exam on topics from lecture.

Literature -
Last update: T_KTI (14.05.2013)

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

Syllabus -
Last update: T_KTI (14.05.2015)

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.

Charles University | Information system of Charles University |