Herbrand Universe
Reduction to Clausal Form
Soundness, Completeness, Consistency, Satisfiability,


Our interest is about: Logic is a crucial tool in Knowledge Representation and Reasoning. In the following we deal with Logic in a fairly formal manner [but, sorry, no proofs here and essentially no examples].

The treatment of Logic in Rich and Knight, Chapter 5, is less complete than desirable. I highly recommend, for the basic ideas and definitions, to look at the course cs157: Logic and Automated Reasoning taught at Stanford by professor Genesereth and at his book Logical Foundations of Artificial Intelligence . You may also look at the lecture notes available for Logic in PAIL. Both PAIL and FLAIR have modules on various aspects of Logic and Theorem Proving. For the utterly devoted to Theorem Proving there is a very powerful tool called Otter.

Logic is a formal system and it is not trivial to covert the statements that we use in normal speech into statements in logic. Here are two examples of english statements that you may wish to convert into a logic language:

(Barwise and Etchemendy) If the unicorn is mythical then it is immortal, but if it is not mythical then it is a mortal mammal. If the uniforn is either immortal or a mammal, then it is horned. The unicorn is magical if it is horned.
(Rich and Knight)
  1. Marcus was a man
  2. Marcus was a Pompeian
  3. All Pompeian were Romans
  4. Caesar was a ruler
  5. All Romans were either loyal to Caesar or hated him
  6. Everyone is loyal to someone
  7. People only try to assassinate rulers they are not loyal to
  8. Marcus tried to assassinate Caesar.

In the following we introduce First Order Logic (FOL), and just mention that it is a generalization of Propositional Logic .


Let us first introduce the symbols, or alphabet, being used. Beware that there are all sorts of slightly different ways to define FOL. Also, beware that I have problems in HTML in writing down some of the logical symbols.



A Term is either an individual constant (a 0-ary function), or a variable, or an n-ary function applied to n terms: F(t1 t2
[We will use both the notation F(t1 t2 and the notation (F t1 t2 .. tn)]

Atomic Formulae

An Atomic Formula is either FALSE or an n-ary predicate applied to n terms: P(t1 t2 .. tn). In the case that "=" is a logical symbol in the language, (t1 = t2), where t1 and t2 are terms, is an atomic formula.


A Literal is either an atomic formula (a Positive Literal), or the negation of an atomic formula (a Negative Literal). A Ground Literal is a variable-free literal.


A Clause is a disjunction of literals. A Ground Clause is a variable-free clause. A Horn Clause is a clause with at most one positive literal. A Definite Clause is a Horn Clause with exactly one positive Literal.
Notice that implications are equivalent to Horn or Definite clauses:
(A IMPLIES B) is equivalent to ( (NOT A) OR B)
(A AND B IMPLIES FALSE) is equivalent to ((NOT A) OR (NOT B)).


A Formula is either: An occurrence of a variable in a formula that is not bound, is said to be free.
A formula where all occurrences of variables are bound is called a closed formula, one where all variables are free is called an open formula.

A formula that is the disjunction of clauses is said to be in Clausal Form. We shall see that there is a sense in which every formula is equivalent to a clausal form.

Often it is convenient to refer to terms and formulae with a single name. Form or Expression is used to this end.


The substitution [t/x] can be seen as a map from terms to terms and from formulae to formulae. We can define similarly [t1/x1 t2/x2 .. tn/xn], where t1 t2 .. tn are terms and x1 x2 .. xn are variables, as a map, the [simultaneous] substitution of x1 by t1, x2 by t2, .., of xn by tn. [If all the terms t1 .. tn are variables, the substitution is called an alphabetic variant, and if they are ground terms, it is called a ground substitution.] Note that a simultaneous substitution is not the same as a sequential substitution. For example, as we will see in the next section,

P(x)[z/x u/z] is P(z), but P(x)[z/x][u/z] is P(u)


The determination of Most General Unifier is done by the Unification Algorithm. Here is the pseudo code for it, and here is the corresponding Lisp code.


Before we can continue in the "syntactic" domain with concepts like Inference Rules and Proofs, we need to clarify the Semantics, or meaning, of First Order Logic.

An L-Structure or Conceptualization for a language L is a structure M= (U,I), where:

The set of functions (predicates) so introduced form the Functional Basis (Relational Basis) of the conceptualization.

Given a language L and a conceptualization (U,I), an Assignment is a map from the variables of L to U.
An X-Variant of an assignment s is an assignment that is identical to s everywhere except at x where it differs.

Given a conceptualization M=(U,I) and an assignment s it is easy to extend s to map each term t of L to an individual s(t) in U by using induction on the structure of the term.

Some of these definitions can be made relative to a set of formulae GAMMA: We say that formulae A and B are (logically) equivalent iff A is a logical consequence of {B} and B is a logical consequence of {A}.

EXAMPLE 1: A Block World

Here we look at a problem and see how to represent it in a language. We consider a simple world of blocks as described by the following figures:
					|a |
					|e |
	+--+				+--+
	|a |				|c |
	+--+	+--+			+--+
	|b |	|d |	======>		|d |
	+--+	+--+			+--+
	|c |	|e |			|b |
      ---------------		--------------------
We see two possible states of the world. On the left is the current state, on the right a desired new state. A robot is available to do the transformation. To describe these worlds we can use a structure with domain U = {a b c d e}, and with predicates {ON, ABOVE, CLEAR, TABLE} with the following meaning: Examples of formulae true in the block world [both in the left and in the right state] are [these formulae are known as Non-Logical Axioms]: Note that there are things that we cannot say about the block world with the current functional and predicate basis unless we use equality. Namely, we cannot say as we would like that a block can be ON at most one other block. For that we need to say that if x is ON y and x is ON z then y is z. That is, we need to use a logic with equality.

Not all formulae that are true on the left world are true on the right world and viceversa. For example, a formula true in the left world but not in the right world is (ON a b).
Assertions about the left and right world can be in contradiction. For example (ABOVE b c) is true on left, (ABOVE c b) is true on right and together they contradict the non-logical axioms. This means that the theory that we have developed for talking about the block world can talk of only one world at a time. To talk about two worlds simultaneously we would need something like the Situation Calculus that we will study later.

Herbrand Universe

It is a good exercise to determine for given formulae if they are satisfied/valid on specific L-structures, and to determine, if they exist, models for them. A good starting point in this task, and useful for a number of other reasons, is the Herbrand Universe for this set of formulae. Say that {F01 .. F0n} are the individual constants in the formulae [if there are no such constants, then introduce one, say, F0]. Say that {F1 .. Fm} are all the non 0-ary function symbols occurring in the formulae. Then the set of (constant) terms obtained starting from the individual constants using the non 0-ary functions, is called the Herbrand Universe for these formulae.

For example, given the formula (P x A) OR (Q y), its Herbrand Universe is just {A}.
Given the formulae (P x (F y)) OR (Q A), its Herbrand Universe is {A (F A) (F (F A)) (F (F (F A))) ...}.

Reduction to Clausal Form

In the following we give an algorithm for deriving from a formula an equivalent clausal form through a series of truth preserving transformations. You can find this algorithm here and the corresponding Lisp code here.
We can state an (unproven by us) theorem:

Theorem: Every formula is equivalent to a clausal form

We can thus, when we want, restrict our attention only to such forms.


An Inference Rule is a rule for obtaining a new formula [the consequence] from a set of given formulae [the premises].

A most famous inference rule is Modus Ponens:

                {A, NOT A OR B}
For example:
		{Sam is tall,
	         if Sam is tall then Sam is unhappy}
		  Sam is unhappy
When we introduce inference rules we want them to be Sound, that is, we want the consequence of the rule to be a logical consequence of the premises of the rule.
Modus Ponens is sound. But the following rule, called Abduction , is not:
		{B, NOT A OR B}
is not. For example:
		John is wet
		If it is raining then John is wet
		It is raining

gives us a conclusion that is usually, but not always true [John takes a shower even when it is not raining].

A Logic or Deductive System is a language, plus a set of inference rules, plus a set of logical axioms [formulae that are valid].

A Deduction or Proof or Derivation in a deductive system D, given a set of formulae GAMMA, is a a sequence of formulae B1 B2 .. Bn such that:

In this case we say that Bn is Derived from GAMMA in D, and in the case that GAMMA is empty, we say that Bn is a Theorem of D.

Soundness, Completeness, Consistency, Satisfiability

A Logic D is Sound iff for all sets of formulae GAMMA and any formula A:

A Logic D is Complete iff for all sets of formulae GAMMA and any formula A:

A Logic D is Refutation Complete iff for all sets of formulae GAMMA and any formula A: Note that if a Logic is Refutation Complete then we can enumerate all the logical consequences of GAMMA and, for any formula A, we can reduce the question if A is or not a logical consequence of GAMMA to the question: the union of GAMMA and NOT A is or not consistent.

We will work with logics that are both Sound and Complete, or at least Sound and Refutation Complete.

A Theory T consists of a logic and of a set of Non-logical axioms.
For convenience, we may refer, when not ambiguous, to the logic of T, or the non-logical axioms of T, just as T.

The common situation is that we have in mind a well defined "world" or set of worlds. For example we may know about the natural numbers and the arithmetic operations and relations. Or we may think of the block world. We choose a language to talk about these worlds. We introduce function and predicate symbols as it is appropriate. We then introduce formulae, called Non-Logical Axioms, to characterize the things that are true in the worlds of interest to us. We choose a logic, hopefully sound and (refutation) complete, to derive new facts about the worlds from the non-logical axioms.

A Theorem in a theory T is a formula A that can be derived in the logic of T from the non-logical axioms of T.

A Theory T is Consistent iff there is no formula A such that both A and NOT A are theorems of T; it is Inconsistent otherwise.
If a theory T is inconsistent, then, for essentially any logic, any formula is a theorem of T. [Since T is inconsistent, there is a formula A such that both A and NOT A are theorems of T. It is hard to imagine a logic where from A and (NOT A) we cannot infer FALSE, and from FALSE we cannot infer any formula. We will say that a logic that is at least this powerful is Adeguate.]

A Theory T is Unsatisfiable if there is no structure where all the non-logical axioms of T are valid. Otherwise it is Satisfiable.

Given a Theory T, a formula A is a Logical Consequence of T if it is a logical consequence of the non logical axioms of T.

Theorem: If the logic we are using is sound then:

  1. If a theory T is satisfiable then T is consistent
  2. If the logic used is also adequate then if T is consistent then T is satisfiable
  3. If a theory T is satisfiable and by adding to T the non-logical axiom (NOT A) we get a theory that is not satisfiable Then A is a logical consequence of T.
  4. If a theory T is satisfiable and by adding the formula (NOT A) to T we get a theory that is inconsistent, then A is a logical consequence of T.