TutorialsArena

Inference in First-Order Logic (FOL): Deducing New Knowledge

Learn about inference in First-Order Logic (FOL), a powerful method for deriving new knowledge from existing facts and logical statements. Explore key concepts like substitution and understand how FOL inference rules enable logical reasoning and problem-solving in artificial intelligence.

Inference in First-Order Logic (FOL)

Introduction

First-order logic (FOL) inference allows us to deduce new facts or sentences from existing ones. Before exploring FOL inference rules, let's understand some key concepts.

Substitution in FOL

Substitution is a fundamental operation in FOL, replacing variables with terms. This is more complex in FOL because of quantifiers (like ∀ and ∃). The notation `F[a/x]` means substituting the constant 'a' for the variable 'x' in the formula F.

(Note: FOL can express facts about specific or all objects in a universe.)

Equality in FOL

Besides predicates and terms, FOL uses equality symbols (=) to state that two terms refer to the same object. The negation of equality (¬(x=y)) means the terms are different.

Examples:

  • Brother(John) = Smith (Brother of John is Smith)
  • ¬(x=y) (x is not equal to y)

FOL Inference Rules for Quantifiers

FOL has inference rules similar to propositional logic:

  • Universal Generalization
  • Universal Instantiation
  • Existential Instantiation
  • Existential Introduction

1. Universal Generalization (UG)

If a premise P(c) is true for an arbitrary element 'c', then ∀x P(x) is also true. (x cannot be a free variable in the premise.)

Example: If "A byte contains 8 bits" is true for any byte, then "All bytes contain 8 bits" is true.

2. Universal Instantiation (UI)

From ∀x P(x), we can infer P(c) by substituting a ground term 'c' (a constant) for 'x'.

Example: If "Every person likes ice cream" (∀x Likes(x, ice cream)), then "John likes ice cream" (Likes(John, ice cream)) is also true.

3. Existential Instantiation (EI)

From ∃x P(x), we can infer P(c) for a *new* constant symbol 'c' that doesn't already appear. 'c' is called a Skolem constant.

Example: From "∃x Crown(x) ∧ OnHead(x, John)," we can infer "Crown(K) ∧ OnHead(K, John)" where K is a new constant.

4. Existential Introduction (or Generalization)

If an element 'c' has property P, then ∃x P(x) is true.

Example: "Priyanka got good marks in English." Therefore, "∃x GotGoodMarks(x, English)."

Generalized Modus Ponens

A key inference rule in FOL, a generalized version of Modus Ponens. If we have P implies Q, and P is true, then Q is true. It uses substitution to match sentences.