4.1 Logic and Logic Programs
- first-order predicate calculus
- Constants (e.g. 1, 99)
- Predicates (evaluate to true or false)
- Functions (evaluate to non boolean values)
- Variables (unspecified quantities)
- 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=
- 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.
4.6 Curry: A Functional Logic Language