Logic and Rules
Expressions in a formal language conform to unambiguous rules of
construction. Inferences are drawn by following strict laws for
manipulating expressions in a formal language The language we use
most often is clausal form logic.
Propositional Calculus
A propositional constant is a symbol (like p, q, r, ...)
that stands for some like ``Sydney is a city''. Propositions are
atomic formulae. A wellformed formula(wff) is defined
as:
if X is atomic then X is a wff
if X is a wff then so is not X
if X and Y are wffs then so is X or Y
X and Y is defined as not(not X or not Y)
(X => Y) is defined as (not X or Y)
(X equiv Y) is defined as (X => Y) and (Y => X)
The letters X and Y are propositional variables
that denote any proposition symbol.
Conjunctive Normal Form
In conjunctive normal form(CNF) we eliminate conditional and
biconditional expressions by converting them to disjunctions.
Negation is moved in so that it only applies to atoms:
not(X and Y) becomes (not X or not Y)
not(X or Y) becomes (not X and not Y)
not not X becomes X
Disjunction is distributed over conjunction using:
(Z or (X and Y)) becomes
((Z or X) and (Z or Y))
Clausal Form
Usually, we reduce arbitrary expressions to clausal form. For example,
not(p or q) => (not p and not q) 
not not(p or q) or (not p and not q)  eliminating =>

(p or q) or (not p and not q)
 driving not in

not p or (p or q)) and (not q or (p or q))  distributing and over or

{{not p, p, q}, {not q, p, q}}
 dropping and and or

The expressions in the braces are either atoms or negated atoms and are called
literals. In clausal form, positive literals are placed to the right of an
arrow symbol and negative atoms to the left. E.g.
p, q < p
p, q < q
In general, a clause is an expression of the form:
p_1, ..., p_m < q_1, ..., q_n
The literals on the left are disjoined conclusions.
The literals on the right are conjoined conditions.
Predicate Calculus
Propositional calculus cannot deal with statements of generality like,
`All men are mortal'.
To do this, we need predicates, arguments, variables and quantifiers. eg.
(forall x)(man(x) => mortal(x))
The Syntax of Predicate Calculus
 Any constant symbol or variable is a term.
 If F_k is a kplace function symbol and a_1, ..., a_k are
terms then F_k(a_1, ..., a_k) is a term.
 If P_k is a kplace predicate symbol and a_1, ..., a_k are
terms then P_k(a_1, ..., a_k) is a wff.
 Negation and disjunction rules are as for propositional calculus.
 If W is a wff and X is a variable then (forall X) W is a wff.
 (exists X) W is defined to be not ((forall X) not W).
FirstOrder Clauses
Like propositional calculus, there is a procedure for converting arbitrary
expressions into clauses.
If a clause has the form p_1, ..., p_m < q_1, ..., q_n and contains
variables x_1, ..., x_k, the interpretation is:
 (forall x_1, ..., x_k), p_1 or ... or p_m is true if q_1 and ... and q_n
are true.
 if n=0 (i.e. no conditions are specified) then p_1 or ... or p_m is true.
 if m= 0 (i.e. no conclusins are specified) then q_1 and ... and q_n is false.
Horn Clauses
A Horn clauseonly has a single positive literal. For example,
p < q_1, ..., q_n
A program in Prolog consists of Horn clause definitions. For example,
on(a, b).
on(b, c).
above(X, Y) : on(X, Y).
above(X, Y), on(Z, Y), above(X, Z).
The Resolution Proof Procedure
To prove p follows from some theory, T, assume not p and then try to derive a
contradiction from its conjunction with T.
Resolution requires a pattern matching
operation, called unification. When matching literals, we look for variable
substititions that will make the two expressions identical. For example,
runs_faster_than(X, zeno)
runs_faster_than(tortoise, Y)
are identical under the substitution {X/tortoise, Y/zeno}.
A clause that contains no variables is called a ground clause.
To resolve two nonground clauses, you must find a unifier for complimentary
literals. For example,
{beats_in_race(X, zeno), not younger_than(X, zeno)}
and
{not beats_in_race(tortoise, Y), not philosopher(Y)}
have unifier U = {X/tortoise, Y/zeno} and generate the resolvent
{not philosopher(zeno), not younger_than(tortoise, zeno)}
We can provea formula, p, if we can derive it from a theory, T by a
sequence of resolution steps. We write this as T  p. Resolution uses a
proof by refutation. That is, add the negation of the goal to the theory and
show that the new theory is inconsistent, ie. implies false. The empty
clause, {}, is interpreted as false. So if theory derives false, we have an
inconsistent theory.
Figure 1: Resolution Proof
Resolution uses backward chainingto focus the search for clauses to
resolve. There are many refinements to this search. Prolog
resolves clauses and their literals in input order, i.e.,
toptobottom, lefttoright.
Soundness and Completness
 A proof procedure is soundif every formula it derives is true.
I.e. it cannot prove something it shouldn't.
 A proof procedure is completeif it can derive every thing
that is possible to derive from a theory. That is, here is no true statement that it cannot prove.
 Decidabilitymeans that we can always show if a proposition
follows from a theory.
 Prolog's proof procedure is sound and complete for Horn clauses.
 Unrestricted firstorder logic is undecidable.
CRICOS Provider Code No. 00098G
Copyright (C) Bill Wilson, 2002, except where another source is acknowledged.
Much of the material on this page is based on an earlier version by
Claude Sammut.