Connectives (operation such as and, or, not and implication … etc)

Quantifiers (universal or existential)

Punctuation Symbols

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

or simply

Unification is the process of pattern matching to make statement identical.

4.4 The Language Prolog

Notation and Syntax

is :-

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=[3]

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).

ancestor(X, X).

parent(amy, bob).

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.