WEEK 8 : First Order Logic

First-order logic is a way of knowledge representation in artificial intelligence. It is an

extension to propositional logic. FOL is sufficiently expressive to represent the
natural language statements in a concise way. First-order logic is also known as
Predicate logic or First-order predicate logic. First-order logic is a powerful language
that develops information about the objects in a more easy way and can also express
the relationship between those objects.

FOL differs from propositional logic (PL), which isn't very expressive because
information can only be represented as either true or false. FOL is an extension of PL
and its predicates assert a relationship among certain elements. It provides a richer
language to mathematically represent linguistic (English) statements. It also requires
more complex mechanisms to check for logical consequences.

FOL is a system of formal logic that provides a way to formalize natural languages
into a computable /mathematical format. With FOL, problems expressed in English
sentences can be represented in a formal manner, which makes it possible to
formulate ideas, draw conclusions and prove theorems. Such formulations support
inferential reasoning, which is crucial for many academic and real-world disciplines,
including:

⚫ mathematics,
⚫ computer programming -- Prolog is based on FOL,
⚫ philosophy,
⚫ science and
⚫ machine learning.

In these fields, FOL is preferred over PL. This is because PL has a limited capacity
for abstraction since it doesn't allow for reasoning over variables and functions having
general and mutable content. FOL provides a more formal logical system that
includes variables and therefore allows for abstraction, symbolic reasoning and
inferences.

First-order logic (like natural language) does not only assume that the world contains
facts like propositional logic but also assumes the following things in the world:

1. Objects: A, B, people, numbers, colors, wars, theories, squares, pits, wumpus, ......
2. Relations: It can be unary relation such as: red, round, is adjacent, or n-any
relation such as: the sister of, brother of, has color, comes between
3. Function: Father of, best friend, third inning of, end of,

As a natural language, first-order logic also has two main parts:

1. Syntax
2. Semantics

Logical and non-logical symbols in first-order logic

FOL syntax can have both logical and non-logical symbols. Logical symbols
correspond to logical operators or connectives, such as ∧, ∨, ¬, ⇒, ⇔. They're always
interpreted in the sense of the logical operation they represent. Also, their meaning is
never conditioned by the domain of discussion in which FOL is used. In other words,
the meaning of a logical symbol in FOL is always unambiguous.

Non-logical symbols in FOL consist of predicates, relationships, constants and

functions. The meaning associated with them is always domain-specific, which is why
their conversion to natural language requires the use of conversion rules and a fair
amount of interpretation.

Example:

In the formula P(x), x could have different meanings depending on the domain:

• In Botany, if P = yellow and x = banana, P(x) = (the) banana is yellow

• In Chemistry, if P = atom and x = oxygen, P(x) = oxygen is (an) atom
• In Mathematics, if P = line and x = infinite, P(x) = (the) line is infinite

Arity in FOL functions and predicates

Arity is the number of arguments, parameters or variables in FOL functions and

predicates. In FOL, each function and predicate symbol has an arity k > 0. An arity of
0 is known as nullary arity. Arities of 1, 2 and 3 are known as unary, binary and
ternary, respectively.

Functions of arity 0 are known as constants. Predicate symbols of arity 0 are

propositions. If a function has arity greater than 0, it could have an infinite number of
terms.

Equality in first-order logic

FOL with equality is an important variant of FOL because it admits equality as a

built-in binary relation symbol, so it's a part of FOL, just like →, ¬ and others. This
differentiates the equality symbol from the function and predicate symbols in a
signature that can be interpreted as arbitrary functions and predicates in a structure.

A special predicate, =, says whether two objects are equal. Equality can only be
applied to objects. To state that two propositions are equal, the ↔ symbol should be
used.
Quantifiers in first-order logic

A quantifier is a tool with the help of which we will be in a position to measure the
magnitude of the subject of a proposition. The term magnitude applies to any physical
quantity which is measurable. In this particular case the measurable physical quantity
is things to which the proposition in question refers. If we translate this term to
traditional mould, then it just signifies the concept of the distribution of terms. The
difference, however, is that in traditional analysis this concept turns out to be quite
clumsy and ambiguous. Various synonymous words make matters further worse. The
use of quantifiers in non-natural language resolves all these difficulties at one stroke.
It is also possible to do away with mathematical interpretation of distribution of terms
if we wish so. Further, this technique renders the application of distribution to the
predicate term superfluous. The significance of the rules of quantification must be
understood against this background.

In FOL, quantifiers allow the definition of formulae where numbers or quantities are
considered in relation to some predicates. They correspond to indefinite adjectives in
the English language, such as any, some, all or none.

Two types of quantifiers are provided in FOL:

• Universal quantifier. A universal quantifier means the statement is true for

everything or every instance of a particular thing within its range. g., for all,
everything, for each, for every.
• Existential quantifier. An existential quantifier expresses that the statement is
true for at least one instance of something within its scope. E.g., for some,
many, at least one

FOL quantifiers are defined through the symbols: ∀ and ∃, which mean all (universal)
and there exists (existential), respectively. Quantifiers always precede variables in the
expressions that contain them and are written as ∀x and ∃x. Also, if the variable refers
to a predicate P(x), the quantifier precedes the predicate and is written as ∀xP(x) and
∃xP(x)

There are four rules of quantification. They are as follows; Universal Instantiation
(UI), Universal generalization (UG), Existential Instantiation (EI.) and Existential
generalization (EG). The first two rules involve the quantifier which is called
Universal quantifier which has definite application. Whenever an affirmative
proposition contains words like ‘all’, ‘every’ ‘each’, etc. and propositions contain
words like ‘No’, ‘None’, etc., universal quantifier replaces all such words. This sort of
economy also achieves simplicity. This is the distinct advantage of the use of
quantifiers. On the other hand, whenever propositions irrespective of quality contain
words like ‘someone’, ‘many things’, ‘a few, etc., existential quantifier is used. In
symbolic logic these quantifiers are symbolized as follows. ‘(x)’ or ‘(∀x)’ is the
symbol for universal quantifier and ‘(∃x)’ is the symbol for existential quantifier. The
symbolic representation of these quantifiers removes ambiguity in addition to
achieving economy and simplicity. The difference between the instantiation and
generalization rules with respect to both the quantifiers is that for universal quantifier
UI allows the elimination of the universal quantifier whereas UG allows us to
introduce a universal quantifier and similarly, for existential quantifier EI allows the
elimination of an existential quantifier and EG allows us to introduce the same.

Rules of Quantification

In predicate calculus the letter ‘x’ signify individual variable. The aforementioned
four rules permit the transformation of non-compound into equivalent compound
propositions to which the Rules of Inference and Equivalence are applicable. They
also permit the transformation of compound propositions into equivalent non-
compound propositions. These additional rules thus make it possible to construct
formal proofs of validity for arguments whose validity depends upon the inner
structure of some non-compound statements contained in those arguments.

Universal Instantiation (UI)

This rule says that any substitution instance of a proposition function can be validly
deduced from a universal proposition. A universal proposition is true only when it has
only true substitution instances. This is the necessary and sufficient condition for any
true universal proposition. Therefore any true substitution instance can be validly
deduced from the respective universal proposition. A propositional function always
consists of variable ‘x’. At times z also is used as a variable and y has a definite role
to play other than that of constant. Therefore any instance which is a substitution for x
is regarded as a constant and letters from ‘a’ through ‘w’ are symbols for constants.
These letters signify subject in traditional sense, and in modern sense, an ‘instance of
a form’. To obtain such an instance of a form ‘x’ is replaced by another Greek letter ‘ν’
(nu) which is another symbol for an individual constant. It is also an example for
universal instantiation because the universal quantifier is instantiated here. This rule is
symbolically represented as follows:
(x) Φx
∴Φ ν3
This rule requires a little elaboration. Let us replace ν by a more familiar constant, say,
a, and Φ by F. When Fa is inferred from (x) Fx, the quantifier (x) is dropped. The
reason is that the universal quantifier has indefinite extension whereas constant is
restricted to one particular individual. Therefore in this context it is wrong to use
universal quantifier. The rule of UI allows such of those instances where we replace
all variables bound by a universal quantifier with individual constant. Thus (x) (Sx =>
Px) will yield (Sa => Pa) where a is the constant used in place of the variable. The
application of UI goes with a few stipulations. The quantifier (x) in (x) Fx should not
be within the range of a negation (¬). It should not also be within the extent of
another quantifier. The span of (x) in (x) Fx must extend to the complete expression.
A violation of any one of these limitations will lead to an incorrect utilization of UI.
In other words, if we say that ¬ (x) Fx implies ¬ Fa, then it must be viewed as a
wrong understanding of UI.
We may use the UI rule in the following way:
a) First, remove the universal quantifier.
b) Next, replace the resulting free variable by a constant.

Universal Generalization (UG)

This rule helps us to proceed to generalization after an arbitrary selection is made to
substitute for x. In UG, ‘arbitrary selection’ is very important because as the name
itself suggests, generalization always proceeds from individual instances. Arbitrary
selection always means ‘any’. And there is no specific choice involved. In this sense,
selection is ‘random’ or arbitrary. The letter y is the symbol of ‘arbitrary’ selection.
This is the reason why ‘y’ is not regarded as a constant. This process is called
generalization because the conclusion is a universal proposition. The underlying
principle is that what holds good in the case of any variable selected at random must
hold good in all instances. In other words, the variable y is equivalent to saying ‘any’.
If we recall the traditional rules of syllogism, universal conclusion follows from
universal premises only. It only means that we need prior universal proposition. Let
us club UI with this step. Then we are allowed to say that if universal proposition is
true then any variable selected at random must be true. Therefore it must be
understood that in this case the process is from universal to universal through an
individual. When ‘x’ replaces ‘y’ there is generalization. When universal quantifier
describes the proposition it becomes UG. The procedure is as follows.
Φy
∴ (x) Φx
In the above given rule the letter ‘y’ in Φy (or Fy) stands for any arbitrarily selected
individual. It is only a pseudo name and not the name of a particular individual. This
letter ‘y’ in UG is not a constant but an individual variable only. But it is different
from x in the sense that it is an indefinite replacement for x. In UG we substitute first
all pseudo names with variables and then bind them with universal quantifiers.
We apply UG to the statement in the following manner:
a) First add the universal quantifier.
b) Then ensure that in the conclusion the variable is bound by this newly introduced
universal quantifier.

Existential Instantiation (EI)

This rule is applicable when the proposition has existential quantifier and in this case
any symbol ranging from a through w is used as a substitute for the individual
variable x. We can infer the truth of any substitution instance from existential
quantification because existential quantification is true only when there is at least one
true substitution instance. However, this rule has a clause when it is applied to an
argument. The constant, say ‘a’ which we use to substitute for x should not have
occurred anywhere earlier in that argument. It only means that in the same argument
EI cannot be used twice when it is assumed that there is only one true substitution
instance. The rule is represented as follows.
(∃x) Φx
∴Φ ν
This formula says that there is at least one or some unspecified number of members in
the
domain in question have a certain property, say, ‘Φ’. The letter ‘ν’ in Φν stands for
that
unspecified number of members and hence it is in a sense sort of pseudo name and not
the name of any particular individual. Therefore this may be called an existential
pseudo name. It is necessary to adhere to certain stipulations while implementing this
rule. In the first place, the formula (∃x) in (∃x) Φx should not be within the range of
negation (¬). Secondly, (∃x) in (∃x) Φx should not be within the extent of another
quantifier. Thirdly, the quantifier (∃x) must cover the complete expression. We may
use the rule EI in a statement in the following way:
a) First, remove the existential quantifier.
b) Next, replace the resulting free variable with a constant.
Existential Generalization (EG)
This rule states that from any true substitution instance of a propositional function, the
existential quantification of that function can be validly deduced. Only then the
existential quantification can become true. When the existential quantification is so
deduced, the individual constant which appeared in earlier steps is replaced by x in
the conclusion. The unique feature of this rule is that though there is generalization,
the conclusion continues to be existential. The rule is represented as follows.
Φν
∴ (∃x) Φ x
In the rule EG the letter ‘ν’ may be the name of a particular individual or again a
pseudo name. (∃x) Φx states that there is at least one x such that x is Φ. When we
apply EG, we have to follow some conditions. Each happening of ‘ν’ in Φ x must be
substituted by ‘x’ and the scope of (∃x) must extend to the entire expression.
The method of application of EG is simple:
a) Insert an existential quantifier.
b) Ensure that at least one occurrence of the individual variable which we have
generalized is bound by the newly introduced existential quantifier.
Earlier, it was stated that the EI should not have occurred earlier in any argument. But
no
explanation was given for this stipulation. We should know why there is this
particular
restriction on the use of EI. Suppose that ‘a’ is the constant whose existence is definite.
We are sure of the existence of a, but we are not sure whether there is any other
constant. In an argument in an earlier step a constant, say, ‘a’ is regarded as ‘b’. The
fact that ‘a’ is ‘b’ is not adequate enough to conclude in some other step that ‘a is c’
when there is no reference of any kind to ‘c’ in the premise. Since the logical constant
‘a’ is used in existential mode, it is mandatory that EI should be used in the very first
step of the proof. If it occupies any other position, then it is a mistake.

RULES OF QUANTIFIER EQUIVALENCE

The standard forms of categorical statements are A, E, I and O. Let us start with A
statement: “Every cat is a mammal.” In this statement there are two individuals, viz.,
‘a cat’ and ‘a mammal. We also know that these propositions are symbolized as
follows.
Cx: x is a cat.
Mx: x is a mammal.
We should also note that the predicate of ‘being a mammal’ is predicated to every
member which has the property of being a cat. We need universal quantifier in this
case. On Boolean interpretation, universal statements are actually conditional
statements with no existential commitment. We may paraphrase it as: For every x, if x
is a cat then x is a mammal. The expression ‘if x is a cat, then x is a mammal’ is
translated with a truth-functional symbol
‘=>’. Thus translated, it becomes (x) (Cx => Mx). Using the same symbolization key,
we symbolize the ‘E’ statement ‘No cat is a mammal’ as, (x) (Cx => ¬ Mx). It must
be remembered that “No cat is a mammal” can be paraphrased as: For every x, if x is
a cat, then x is not a mammal. This proposition does not deny the predication of the
property of ‘being a cat’, but it denies the property of ‘being a mammal’ to any cat.
This is the reason why the negation sign is placed before ‘Mx’ in the statement ‘(x)
(Cx => ¬ Mx)’.

Let us consider the ‘I’ and ‘O’ statements. ‘Some cats are mammals’ is an illustration
for ‘I’. When paraphrased, we have to admit the existential import and also the
property predication. It has to be stronger in assertion than the conditional we state for
the universal statements. Considering these aspects, we translate I and O propositions
to symbolic form. There is (exists) at least one x such that x is a cat and x is a
mammal. This is symbolized as follows:
(∃x) (Cx Λ Mx)

Note that a truth-functional symbol ‘Λ’ from propositional logic has been used to
denote that both properties belong to ‘x’. We translate the ‘O’ statement, ‘Some cats
are not mammals’ in the following way. There is (exists) at least one x such that x is a
cat and x is not a mammal; and this expression is symbolized as follows:
(∃x) (Cx Λ ¬ Mx)

As a matter of convention these propositions are represented symbolically as follows:

1. (A) (x) Φx
2. (E) (x) ¬ Φx
3 (I) (∃x) Φx
4 (O) (∃x) ¬ Φx

Using class membership relation, these propositions are represented as follows:

1. (x) Φx ≡ (x){x є Φ => x є Ψ} Where є is read ‘element of’
2. (x) ¬ Φx ≡ (x){x є Φ => x є Ψ} Where є is read ‘not an element of’
3. (∃x) Φx ≡ (∃x){x є Φ Λ x є Ψ}
4. (∃x) ¬ Φx ≡ (∃x){x є Φ Λ x є Ψ}

Where Φ and Ψ are the symbols for attributes. These are the four rules of quantifier
equivalence. They are also known as Quantifier Negation Rules because if negation is
placed behind quantifier, then it becomes the contradiction of the original statement.

I. We shall apply ‘UI’ for the statements mentioned below and remove the quantifier.
a) (x) (Hx => Mx)
___________
(Ha => Ma)

b) (x) (Hx => ¬ Mx)

___________
(Ha => ¬ Ma)

c) (x) (Mx => ¬ Ix)

___________
(Ma => ¬ Ia)

II. We shall now apply ‘UG’ for the statements mentioned below to add quantifier and
then
generalize. Very soon we ought to discover that this is really the reverse process.
d) (Ha => Ma)
___________
(x) (Hx => Mx)

e) (Ha => ¬ Ma)

___________
(x) (Hx => ¬ Mx)

f) (Ma => ¬ Ia)

___________
(x) (Mx => ¬ Ix)

III. We shall apply ‘EI’ for the statements mentioned below to remove the quantifier.
g) (∃x) (Hx Λ Mx)
___________
(Ha Λ Ma)

h) (∃x) (Hx Λ ¬ Mx)

___________
(Ha Λ ¬ Ma)

i) (∃x) (Mx Λ ¬ Ix)

___________
(Ma Λ ¬ Ia)

IV. We shall apply EG for the statements mentioned below to add quantifier and to
generalize:
j) (Ha Λ Ma)
___________
(∃x) (Hx Λ Mx)

k) (Ha Λ ¬ Ma)
___________
(∃x) (Hx Λ ¬ Mx)

l) (Ma Λ ¬ Ia)
___________
(∃x) (Mx Λ ¬ Ix)

Examples

1. Symbolize the following using universal quantifier.

a) Every Human is a mammal

(x) (Hx => Mx)

b) No Horse is a mammal.
(x) (Hx => Mx)

c) All dogs are four legged.

(x) (Dx => Fx)
d) No donkeys are birds.
(x) (Dx=> ¬ Bx)

e) No men are immortal.

(x) (Mx=> ¬ Ix)

2. Symbolize the following using existential quantifier.

a) Some flowers are red.

(∃x) (Fx Λ Rx)

b) Some flowers are not red.

(∃x) (Fx Λ ¬ Rx)

c) Some birds are White.

(∃x) (Bx Λ Wx)

d) Some fish are not snake.

(∃x) (Fx Λ ¬ Sx)

e) Some men are tall.

(∃x) (Mx Λ Tx)

Consider the following proposition.

1. All spinsters are unmarried female persons.

∴ All unmarried female persons are spinsters.
Since the rule of distribution is adhered to, the argument is valid. Let us see how the
rule of
quantification can be applied to this example.
There are two ways of symbolizing. They are as follows
a) (x){x є S => x є U}
b) (x){ x є S <=> x є U}
a) does not completely convey the meaning of 1. Therefore we have to consider b). It
can be reformulated as follows:
c) (x){ x є S => x є U} Λ { x є U => x є S }
For the sake of simplicity let us drop the quantifier. Applying commutative law, we
get
d) { x є U => x є S } Λ { x є S => x є U}
This is an instance of simple conversion. Now apply simplification law.
e) { x є U => x є S }
Translate ‘e’ to natural language. All unmarried female persons are spinsters.
It may be noted that if this method is followed, we do not get the existential
conclusion.
Therefore conversion by limitation does not find place in this interpretation. (It is
possible to get the identical result if commutative law is not used. But then it will not
be clear to an untrained mind that the proposition is converted. It must be noted that
commutative law is nothing but conversion). Examination of E proposition is left for
the student as an exercise. The case of existential proposition is simple. Examine this
statement.

3. Some bananas are sweet.

Translate this statement to symbolic form.

a) (∃x) {(x є B) Λ (x є S)}
Again, drop the quantifier for the sake of simplicity and apply commutative law. We
get
b) {(x є S) Λ (x є B)}
When b) is translated to natural language, we get conversion in traditional sense.
Some sweet objects are bananas.
The case of O is a special case. It is quite illuminating to apply the quantification rules
to know why it does not have conversion.

3. Some bananas are not sweet.

Translate this statement to symbolic form.
a) (∃x) {Bx Λ ¬ Sx}
(For the sake of simplicity class-membership is not considered in this particular case).
In this case simple conversion is possible in a different way altogether. We can only
say (∃x) {¬ Sx Λ Bx} If we reflect for a while we easily discover that this is, in reality,
the symbolic form of partial contraposition. Suppose that we restrict ourselves to
conversion. We are only entitled to convert (or commute) Bx and Sx. The negation
sign ought to remain unaffected. For further clarity, let us compare the scene with
algebra. a + b = - c becomes c = - (a + b). Just as negative sign is not disturbed in
algebra while interchanging, so also in modern logic the negation sign remains
undisturbed when we interchange the terms. But this is not conversion. In the case of
algebraic equation, signs on both sides change. Therefore it is not equivalent to
commutation. Commutation and conversion are technically identical. The upshot of
the argument is that when there is negation on any one side or term, conversion or
commutation is not possible. In other words, commutation holds good only when the
relation is symmetric. On similar lines, obversion can be explained. If x is not an
element of S, then it means that x is an element of the complement of S.
The position of equivalence relation has now become clear. We have learnt that along
with quantification rules we also require Rules of Inference and Rules of Replacement.
We use the same technique to test the validity of syllogism. It is a matter of great
interest to know that the rules of quantification project syllogism in a new perspective,
which helps us to abandon the rule of distribution of terms, which is not only
cumbersome in presentation but also time consuming. Further, quantification rules
can be used to test non-syllogistic arguments also subject to the condition that general
and singular propositions find place in such arguments.

Let us use the following arguments to illustrate these rules.

1.
1) All Indians are Asians.
2) Tendulkar is an Indian.
3) ∴Tendulkar is an Asian.
This is symbolized as follows: (x) {Ix => Ax}
It
∴At
The formal proof is constructed as follows:
1) (x){Ix => Ax}
2) It / ∴At
3) It => At 1, UI
4) ∴At 3, 2, M.P.
In this particular argument only one premise is general. However, the argument may
consist of only general proposition in which case slightly different procedure has to be
followed. Consider this argument.

2.
1) All citizens are voters.
2) All ministers are citizens.
3) ∴All ministers are voters.
When symbolized it becomes:
1) (x){Px => Vx}
2) (x){Mx => Px} / ∴ (x){Mx => Vx}
The formal proof is as follows:
1) (x){Px => Vx}
2) (x){Mx => (Px} / ∴ (x){Mx => Vx}
3) Pa => Va 1, UI
4) Ma => Pa 2, UI
5) Ma => Va 4, 3, H.S.
6) ∴ (x){Mx => Vx} 5, UG

When the individual variable x is instantiated by any constant, then quantifier goes
and we do not quantify individual or individuals. Now coming to the 6th step, it may
be mentioned that if one substitution instance is true for a given structure then all
substitution instances must be true for that structure. Further the universal
quantification of a propositional function is true if and only if all substitution
instances are true. (The 6th line is not a part of the proof). In the third and the fourth
steps we have applied universal instantiation because both premises are universal and
therefore we have substituted the constants for variables.

UG can be applied in the following manner. Add the sixth line to the proof system
after we replace x by y at all stages. Then we have the application of UG

1) (x){Px => Vx}

2) (x){Mx => Px} / ∴ (x){Mx => Vx}
3) Py => Vy 1, UI
4) My => Py 2, UI
5) My => Vy 3, 4, H.S.
6) ∴ (x){Mx => Vx} 5 UG

These two examples suggest that while testing the validity of arguments in general, UI
has to be used necessarily though EI may not be necessary. The situation is similar to
the traditional formation of rules of syllogism, which hint that without particular
propositions it is possible to construct an argument, but not without universal
propositions.

Now consider an argument, which has a particular proposition. Since one proposition
is particular, it is imperative that the conclusion must be particular.

3.
1) All citizens are voters.
2) Some ministers are citizens.
∴Some ministers are voters.
By now the method of symbolization should be familiar.
1) (x){Px => Vx}
2) (∃x{Mx Λ Px} / ∴ (∃x{Mx Λ Vx}
3) Ma Λ Pa 2, E.I.
4) Pa => Va 1, UI
5) Pa Λ Ma 3, Com.
6) Pa 5, Simp.
7) Ma 5, Simp.
8) Va 4, 6, M.P.
9) Ma Λ Va 7, 8, Conj.
10) ∴ (∃x)(Mx Λ Vx) 9, UG

Let us examine why the restriction of EI must be honoured. Consider a fallacious

argument.

1) Some animals are herbivorous.

2) Some animals are men.
∴Some men are herbivorous.
When symbolized the argument becomes:

1) (∃x){Ax Λ Hx}
2) (∃x){Ax Λ Mx} / ∴ (∃x)(Mx Λ Hx)
3) Aa Λ Ha 1, E.I.
4) Aa Λ Ma 2, E.I. (Error)

4th Step is erroneous. The second premise tells us that there is at least one thing that is
both an animal and herbivorous. It does not permit us to conclude it should also be
regarded as man. Therefore a second use of EI leads to error

Resolution

Steps for Resolution:

 1. Conversion of facts into first-order logic.
2. Convert FOL statements into CNF
3. Negate the statement which needs to prove (proof by contradiction)
4. Draw resolution graph (unification).

To better understand all the above steps, we will take an example in which we will
apply resolution.

Example:

1. John likes all kind of food.

2. Apple and vegetable are food
3. Anything anyone eats and not killed is food.
4. Anil eats peanuts and still alive
5. Harry eats everything that Anil eats.
Prove by resolution that:
6. John likes peanuts.

Step-1: Conversion of Facts into FOL

In the first step we will convert all the given statements into its first order logic.

Step-2: Conversion of FOL into CNF

In First order logic resolution, it is required to convert the FOL into CNF as CNF
form makes easier for resolution proofs.

• Eliminate all implication (→) and rewrite

1. ∀x ¬ food(x) V likes(John, x)
2. food(Apple) Λ food(vegetables)
3. ∀x ∀y ¬ [eats(x, y) Λ ¬ killed(x)] V food(y)
4. eats (Anil, Peanuts) Λ alive(Anil)
5. ∀x ¬ eats(Anil, x) V eats(Harry, x)
6. ∀x¬ [¬ killed(x) ] V alive(x)
7. ∀x ¬ alive(x) V ¬ killed(x)
 8. likes(John, Peanuts).

• Move negation (¬)inwards and rewrite

9. ∀x ¬ food(x) V likes(John, x)
10. food(Apple) Λ food(vegetables)
11. ∀x ∀y ¬ eats(x, y) V killed(x) V food(y)
12. eats (Anil, Peanuts) Λ alive(Anil)
13. ∀x ¬ eats(Anil, x) V eats(Harry, x)
14. ∀x ¬killed(x) ] V alive(x)
15. ∀x ¬ alive(x) V ¬ killed(x)
16. likes(John, Peanuts).

• Rename variables or standardize variables

1. ∀x ¬ food(x) V likes(John, x)
2. food(Apple) Λ food(vegetables)
3. ∀y ∀z ¬ eats(y, z) V killed(y) V food(z)
4. eats (Anil, Peanuts) Λ alive(Anil)
5. ∀w¬ eats(Anil, w) V eats(Harry, w)
6. ∀g ¬killed(g) ] V alive(g)
7. ∀k ¬ alive(k) V ¬ killed(k)
8. likes(John, Peanuts).

• Eliminate existential instantiation quantifier by elimination.

In this step, we will eliminate existential quantifier ∃, and this process is
known as Skolemization. But in this example problem since there is no
existential quantifier so all the statements will remain same in this step.
• Drop Universal quantifiers.
In this step we will drop all universal quantifier since all the statements are not
implicitly quantified so we don't need it.

1. ¬ food(x) V likes(John, x)
2. food(Apple)
3. food(vegetables)
4. ¬ eats(y, z) V killed(y) V food(z)
5. eats (Anil, Peanuts)
6. alive(Anil)
7. ¬ eats(Anil, w) V eats(Harry, w)
8. killed(g) V alive(g)
9. ¬ alive(k) V ¬ killed(k)
10. likes(John, Peanuts).

Note: Statements "food(Apple) Λ food(vegetables)" and "eats (Anil, Peanuts) Λ

alive(Anil)" can be written in two separate statements.

• Distribute conjunction ∧ over disjunction ¬.

This step will not make any change in this problem.

Step-3: Negate the statement to be proved

In this statement, we will apply negation to the conclusion statements, which will be
written as ¬likes(John, Peanuts)

Step-4: Draw Resolution graph:

Now in this step, we will solve the problem by resolution tree using substitution. For
the above problem, it will be given as follows:

Hence the negation of the conclusion has been proved as a complete contradiction
with the given set of statements.

Explanation of Resolution graph:

• In the first step of resolution graph, ¬likes(John, Peanuts) , and likes(John, x)

get resolved(canceled) by substitution of {Peanuts/x}, and we are left with ¬
food(Peanuts)
• In the second step of the resolution graph, ¬ food(Peanuts) , and food(z) get
resolved (canceled) by substitution of { Peanuts/z}, and we are left with ¬
eats(y, Peanuts) V killed(y) .
• In the third step of the resolution graph, ¬ eats(y, Peanuts) and eats (Anil,
Peanuts) get resolved by substitution {Anil/y}, and we are left with
Killed(Anil) .
• In the fourth step of the resolution graph, Killed(Anil) and ¬ killed(k) get
resolve by substitution {Anil/k}, and we are left with ¬ alive(Anil) .
• In the last step of the resolution graph ¬ alive(Anil) and alive(Anil) get
resolved.