Connectives (operation such as and, or, not and implication … etc)
Quantifiers (universal or existential)
4.2 Horn Clauses
Horn clause is a statement of the form: where b is called the head and a’s are the body.
Without the body, b is an axiom or facts.
4.3 Resolution and Unification
Resolution is an inference rule: For example
if matches a, then
Unification is the process of pattern matching to make statement identical.
4.4 The Language Prolog
Notation and Syntax
uppercase is variable
lowercase is name of predicates and functions
and is comma (,)
or is semicolon (;)
[x, y, z] is a list with element x, y and z.
If [H|T] = [1, 2, 3], then H=1 and T=[2,3]. If [X, Y|Z] = [1,2,3], then X=1, Y=2 and Z=
empty list is 
=< and => are “less than and equal to” and “greater than and equal to”
! is cut. Freeze a choice when
To force evaluation to get equality of value, use “is”. Otherwise, “=” will result in something like this
3 + 5 = 8 evaluate to no (or false)
Unification algorithm for Prolog
constant unifies only with itself
uninstantiated variable unified with anything and become instantiated to that thing
structured term unifies with another term only if it has the same function name and the same number of arguments. E.g. f(a,X) unifies with f(Y,b) where X=b and Y=a.
Prolog search strategy is to replacing the goals left to right, and consider the clause from top to bottom. This is problematic for the following will cause infinite loop because Prolog will attempt to satisfy ancestor(Z, Y) by reusing the first clause. Switching the two predicate on the right side of the first clause fixes the problem.
ancestor(X, Y) :- ancestor(Z, Y), parent(X, Z).
Cut can be used to imitate if-else. D = if A then B else C
D :- A, !, B.
D :- C.
4.5 Problem with Logic Programming
occur-check problem is when unifying a variable with a term, Prolog does not check whether the variable occurs in the term it is being instantiated to. E.g. is_own_successor :- X = successor(X).
not(not(something(X))) will succeed if not(something(X)) fail. But once not(something(X)) fail, X becomes uninstantiated.