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 well-formed 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 bi-conditional 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 k-place function symbol and a_1, ..., a_k are terms then F_k(a_1, ..., a_k) is a term.
If P_k is a k-place 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).

First-Order 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 non-ground 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., top-to-bottom, left-to-right.

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 first-order 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.