Logic
  Language
  Interpretation
  Model
  Logical consequence
  Soundness and completeness

Definite programs
  Syntax (rules, facts, goals/queries)
  Herbrand universe/base/interpretation
  Least Herbrand model
  Fixed point semantics
  Immediate consequence operator

SLD-resolution
  Substitutions
  Unification
  Most general unifier
  Unification algorithm
  SLD-derivation
  SLD-tree
  Computation rule
  Soundness and completeness

Negation
  Closed world assumption
  Negation as (finite) failure
  Completion
  General logic programs
  SLDNF-resolution
  SLDNF-forest
  Soundness and completeness

Cut

Definite clause grammars
  Translation to Prolog

Prolog
  Databases
  Recursive data structures
  Lists and difference lists
  Simple analysis
  Constraints (especially FD-constraints)