FOL Inference Algorithms

First Order Logic

General Overview

  • Course Information:

    • Course Code: CSC-4240/5240

    • Course Title: ARTIFICIAL INTELLIGENCE

    • Instructor: Amr Hilal, Associate Professor

    • Semester: Fall 2025

    • Date: 10/9/2025

Key Terms and Notations

Terms and Examples

  • Example Substitutions:

    • Glitter(x,y) → Glitter(3,3)

    • Adjacent(x,2,2,y) → Adjacent(2,y,x,3)

    • At(w,x,y) → At(Wumpus,u,3)

    • At(Agent,x,Row(Wumpus))

    • At(z,3,Row(w))

    • Glitter(Row(y), y) → Glitter (x, x)

Unification Examples

  • Successful Examples:

    • {x/3, y/3}

  • Failed Examples:

    • {w/Wumpus, x/u, y/3}

    • {z/Agent, x/3, w/Wumpus}

  • View on Occur-check: The occur-check validates whether a variable occurs in a specific term during unification, which can fail certain unifications.

Recap of First Order Logic (FOL) Inference Techniques

Core Inference Techniques

  1. Reduction to Propositional Logic (PL):

    • Utilize previously established methods to infer conclusions from propositional logic.

  2. Lifted Inference:

    • Searching for more general inference rules that can be applied to First Order Logic (FOL).

    • Includes:

      • Generalized Modus Ponens (GMP)

      • Unification

  3. Discussion on Inference Algorithms:

    • Apply inference rules to ascertain the truth of a given goal in FOL.

FOL Syntax and Clause Definitions

Logical Structures

  • Definite Clauses:

    • Definition: A disjunction of literals that contains exactly one positive literal.

    • Example:

      • The clause ¬A v ¬B v ¬C v D is equivalent to A ∧ B ∧ C ⇒ D.

    • Note: Some logical sentences may not conform to the structure of definite clauses and cannot effectively use forward chaining.

Forward Chaining Technique

Mechanism of Forward Chaining

  • Definition:

    • Starts with atomic sentences (facts) in the knowledge base (KB).

    • Generalized Modus Ponens (GMP) is used to apply all implication rules whose conditions are satisfied by the current atomic sentences, allowing inference of new atomic sentences.

    • The process continues until no new facts are derived or the goal is met.

Example Proof Structure

  1. Premises:

    • If X is a parent of Y, then X is older than Y.

      • orallx,yextParent(x,y)<br>ightarrowextOlder(x,y)orall x,y ext{ Parent}(x,y) <br>ightarrow ext{Older}(x,y)

    • If X is the mother of Y, then X is a parent of Y.

    • Lulu is the mother of Fifi.

  2. Goal: Prove Older(Lulu, Fifi)

  3. Application:

    • By GMP using substitution θ = {x/Lulu, y/Fifi}, sequentially apply rules to derive the goal.

Legal Example and Setup

Crime and Weapon Selling Scenario

  • Statement: It is illegal for an American to sell weapons to hostile nations.

    • Clauses:

    • orall x, y, z ig[( ext{American}(x) igwedge ext{Weapon}(y) igwedge ext{Hostile}(z) igwedge ext{Sells}(x,z,y))
      ightarrow ext{Criminal}(x)ig]

    • Fact Generation:

    • Nono has missiles, interpreted as:

    • orall x ext{ Owns}(Nono,x) igwedge ext{Missile}(x)

    • Represent through existential instantiation resulting in definite clauses.

Iterative Proof Process

  1. Count and convert rules into atomic sentences for application.

  2. Identify relationships in statements through iterative unification techniques.

  3. Derive new conclusions based on generalized rules.

Properties of Forward Chaining

Analysis of Characteristics

  1. Soundness:

    • Each inference accurately follows the applications of GMP.

  2. Completeness:

    • It successfully responds to every query entailed by definite clauses.

  3. Complexity:

    • Algorithms face challenges with clauses containing function symbols as they can lead to infinitely new facts.

    • Datalog defines a workable language involving first-order definite clauses without functions, enhancing termination.

Backward Chaining Technique

Mechanism Overview

  • Definition:

    • A method that seeks to prove the premises by working backward from the goal.

    • Creates new recursive calls to check premises of the rules leading to each goal in a depth-first search (DFS) manner.

Example Steps in Backward Chaining

  1. Bind to a specific case such as orall x, y, z ig[( ext{American}(x) igwedge ext{Weapon}(y) igwedge ext{Hostile}(z) igwedge ext{Sells}(x,z,y))
    ightarrow ext{Criminal}(x)ig]

  2. Trigger various recursive calls based on known premises and rules until the final goals are resolved.

  3. Evidence suppression through logical regressions confirms or denies criminal implications.

Resolution in First Order Logic

Fundamentals

  • Applicability:

    • Resolution is adaptable beyond definite clauses, operational when managing various knowledge bases.

  • Recall:

    • Complements prior resolution definitions established in propositional logic involving complementary literals.

Resolution Example Walkthrough

  • Base Facts:

    • The transformation of statements into conjunctive normal forms (CNF) prepares the inference process.

    • Successful application demonstrates that resolution can prove entailed sentences by deriving contradictions with negated statements.

Proof By Refutation Using Resolution

  1. Process involves systematically converting and negating statements into CNF before applying resolution.

  2. Identifies contradictions to establish the validity of a specific conclusion.

Homework Exercise

Assignment

  1. Given the sentences involving pigs, slugs, and their relations, implement backwards chaining to prove:

    • Faster(Pat, Steve)