Logic
Language
Interpretation
Model
Logical consequence
Soundness and completeness
Definite programs
Syntax (rules, facts, queries/goals)
Proof trees
Atomic logical consequences of a program (proof tree roots)
Correctness and completeness (of a program) w.r.t. a specification
Incorrectness diagnosis, incompleteness diagnosis
Herbrand universe/base/interpretation
Least Herbrand model
Immediate consequence operator
SLD-resolution
Substitutions
Unification
Most general unifier
Unification algorithm
SLD-derivation
SLD-tree
Selection rule (computation rule)
Soundness and completeness
Negation
Closed world assumption
Negation as (finite) failure
Completion
General logic programs
SLDNF-resolution
SLDNF-forest
Soundness and completeness
Definite clause grammars
Translation to Prolog
Prolog
Recursive data structures
Lists and difference lists
Constraints (especially FD-constraints)
The cut
[Version 2.0 of 2013]