Sylabus
Vztah SLD rezoluce k čistému Prologu. Domény, konečné domény.
Zastavování výpočtů, stupňová zobrazení, omezené dotazy.
Occur-check, mody, lineární termy.
Částečná korektnost, podmíněné dotazy a programy, před- a po-podmínky.
Negativní informace. Nemonotonní odvozování, hypotéza uzavřeného světa, odvozovací pravidlo "Negace jako neúspěch". Charakterisace konečného neúspěchu.
Zúplnění logického programu. Přechod od logického programu P s negací k jeho zúplnění, programy IF(P), IFF(P) a zúplnění. Korektnost pravidla negace definované neúspěchem. Úplnost pravidla negace definované neúspěchem.
Argumentace.
Anotace
Prolog a jeho řídící struktury, domény a datové struktury. Sémantika programů.
Konečnost výpočtů, stupňová zobrazení. Test konfliktu proměnných.
Dokazování správnosti programů. Negativní informace, pravidlo "Negace jako neúspech", nemonotónní odvozování.