Sylabus
Ú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.
Anotace
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.