Reasoning Using First Order Logic

Here,  Study of Representation of FOL and Reasoning of FOL.

Sentences

A predicate is a sentence

If sen, sen' are sentences & x a variable, then
      (sen), ㄱsen, ∃x sen, ∀x sen, 
sen ⋀ sen', sen ⋁ sen', sen ⇒ sen'
are sentences

Nothing else is a sentence

Examples of Sentences

Birthday (x, y) - x celebrates birthday on date y

∀y ∃x Birthday (x, y) -
  For all dates, there exists a Person who celebrates his/her Birthday on that date.

Brother(x, y) - x is y's brother
Loves (x, y) - x loves y
     ∀x ∀y Brother (x, y) ⇒ Loves (x, y)
Everyone loves (all of ) his/her brothers.

Let m(x) represent mother of x then "everyone loves his/her mother" is
                   ∀x Loves (x, m(x) )

Any number is the successor of its predecessor

succ (x), pred (x),
 equal (x, y)
      ∀x equal (x, succ (pred (x) )

Alternative Representation

The Above example can be represented succinctly as
    ∀x (succ ( pred (x) = x)

FOL with Equality

• In FOL with equality, we are allowed to use the equality sign (=) between two functions.
• This is just for representational ease
• We modify the definition of sentence to include equality as 

              term = term is also a sentence

Quiz Revisited

• Some dogs bark
• ∃x (dog(x) ∧ bark(x) )

• All dogs have four legs
• ∀x (dog(x) ￫ have_four_legs (x)
• ∀x (dog(x) ￫ legs (x, 4)

• All barking dogs are irritating Do it yourself
• No dogs purr

       ㄱ ∃x (dog(x) ∧ purr(x) )

•  Father are male parents with children

         ∀x (father(x) ⇾ male(x) ⋀ has_children(x) )

• Students are people who are enrolled in courses

 Inference Rules

Universal Elimination 

    ∀x Likes (x, flower)

substituting x by Shirin gives

    Likes (Shirin, flower)

The substitution should be done by a constant term

 Existential Elimination (Skolemization)

   ∃x Likes (x, flower) ⇒ Likes (Person, flower)

   as long as person is not in the knowledge base

Existential Introduction

     Likes (Shahid, flower)

 Can be written as

    ∃x Likes (x, flower)

Reasoning in FOL

Consider the following problem :

If a perfect square is divisible by a prime p, then it is also divisible by square of p.

Every perfect square is divisible by some prime.

36 is a perfect square.

Does there exist a prime q such that square of q divides 36?

Representation in FOL

If a perfect square is divisible by a prime p, then it is also divisible by square of p. 
  ∀x,y perfect_sq (x) ∧ prime (y) ∧ divides (x,y) 
        ⇒ divides (x, square (y) )

 Every perfect square is divisible by some prime.
    ∀x ∃y perfect_sq (x) ⋀ prime (y) ⋀ divides (x,y)

36 is a perfect square
            perfect_sq (36)

Does there exist a prime q such that the square of q divides 36 ?
   ∃y prime (y) ⋀ divides (36, square (y) )

The Knowledge base

1. ∀x,y perfect_sq (x) ⋀ prime (y) ⋀ divides (x,y) ⇒ divides (x, square (y) )

2. ∀x ∃y perfect_sq (x) ⋀ prime (y) ⋀ divides (x,y)

3. perfect_sq (36)