Logické programování 1 - NAIL076

• Anglický název: Logic Programming 1
• Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2020
• Semestr: zimní
• E-Kredity: 3
• Rozsah, examinace: zimní s.:2/0, Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština
• Způsob výuky: prezenční
• Garant: doc. Mgr. Petr Gregor, Ph.D.; RNDr. Jan Hric
• Vyučující: RNDr. Jan Hric
• Třída: Informatika Mgr. - Teoretická informatika; Informatika Mgr. - Diskrétní modely a algoritmy
• Kategorizace předmětu: Informatika > Programování, Teoretická informatika
• Je korekvizitou pro: NAIL077

Anotace

čeština

Hornova logika, logické programy, procedurální interpretace logických programů, Prolog a jeho řídící struktury, semantika programů, ukončení práce programu, test konfliktu proměnných.

Poslední úprava: T_KTI (12.05.2004)

angličtina

Horn logic, logic programs, procedural interpretation of logic programs, Prolog and its procedures, semantics of logic programs, Termination, Occur-check

Poslední úprava: T_KTI (12.05.2004)

Cíl předmětu

čeština

Naučit teorii a techniky používané v logickém programování

Poslední úprava: T_KTI (26.05.2008)

angličtina

To learn theory and techniques used in logic programming.

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

Podmínky zakončení předmětu

čeština

Na ústní zkoušce s přípravou prokázat znalost přednesených témat.

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

angličtina

Oral exam on topics from lecture.

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

Literatura

čeština

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

Poslední úprava: Hric Jan, RNDr. (23.10.2012)

angličtina

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

Poslední úprava: T_KTI (14.05.2013)

Sylabus

čeština

Úvod. Hornova logika jako fragment predikátové logiky I. řádu, syntaktický popis Hornových klausulí a logických programů.

Substituce a unifikace. Unifikační substituce a unifikační algoritmus. Idempotentní a relevantní substituce.

Výpočetní proces, SLD-resoluce. Resoluční krok, SLD-derivace a jejich vlastnosti, lemma o variantách. Resoluční zamítnutí, SLD-stromy.

Úplnost SLD-resoluce. Substituční lemma, množina úspěchů logického programu, její vztah k nejmenšímu Herbrandovu modelu. Věta o úplnosti SLD-resoluce.

Odpovědní substituce. Korektní odpovědní substituce, silná úplnost SLD-resoluce, charakterisace množiny úspěchů logického programu.

Sémantika logických programů. Korektnost SLD-resoluce, Herbrandovy modely logických programů, operátor bezprostředního důsledku, operátory a pevné body. Nejmenší Herbrandův model a jeho charakterizace.

Poslední úprava: T_KTI (14.05.2015)

angličtina

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.

Poslední úprava: T_KTI (14.05.2015)