Artificial Intelligence: Inference Rules in First Order Logic

In Artificial Intelligence (AI), particularly in Knowledge Representation and Reasoning (KRR), inference rules in First Order Logic (FOL) are used to derive new knowledge from existing knowledge (facts and rules). These inference rules enable automated reasoning systems (like logic engines or theorem provers) to simulate intelligent behavior.


What is First Order Logic (FOL)?

FOL extends Propositional Logic by:

  • Introducing quantifiers:

    • Universal (∀): "for all"

    • Existential (∃): "there exists"

  • Allowing variables, functions, and predicates, enabling expression of more complex statements.


Common Inference Rules in First Order Logic

Here are the core inference rules used in FOL:

1. Universal Instantiation (UI)

From a universally quantified statement, infer the statement for a specific individual.

Rule:
∀x P(x) ⟹ P(a)

Example:

∀x Human(x) → Mortal(x)
⟹ Human(Socrates) → Mortal(Socrates)

2. Existential Instantiation (EI)

From an existential statement, introduce a specific but arbitrary constant (Skolem constant).

Rule:
∃x P(x) ⟹ P(c), where c is a new constant

Example:

∃x Loves(x, Juliet)
⟹ Loves(Romeo, Juliet) (assuming Romeo is the chosen constant)

3. Universal Generalization (UG)

From a statement about an arbitrary individual, infer a universal statement.

Rule:
P(x) (for arbitrary x) ⟹ ∀x P(x)

Note: Only valid when x is not dependent on any assumptions.

4. Existential Generalization (EG)

From a specific instance, infer that the property holds for at least one element.

Rule:
P(a) ⟹ ∃x P(x)

Example:

Mortal(Socrates) ⟹ ∃x Mortal(x)

5. Modus Ponens (MP)

Classic inference from propositional logic, also valid in FOL.

Rule:
P, P → Q ⟹ Q

Example:

Human(Socrates), Human(x) → Mortal(x) ⟹ Mortal(Socrates)

6. Resolution (for FOL)

Main rule used in automated theorem proving. It requires all statements to be in clause form (Conjunctive Normal Form).

Rule:
From: (A ∨ B), (¬B ∨ C) ⟹ (A ∨ C)

Steps Involved:

  1. Convert statements to prenex form

  2. Eliminate implications, move quantifiers outward

  3. Skolemization (remove existential quantifiers)

  4. Convert to CNF

  5. Apply resolution recursively until contradiction or solution found


Example: Applying Inference Rules

Given:

  1. ∀x (Human(x) → Mortal(x))

  2. Human(Socrates)

Goal: Prove Mortal(Socrates)

Steps:

  • Apply UI on (1): Human(Socrates) → Mortal(Socrates)

  • Apply MP using (2): ⟹ Mortal(Socrates)


Use in AI Applications

  • Theorem proving

  • Expert systems

  • Natural language understanding

  • Planning and problem-solving