FOL Inference

Inference in First Order Logic

• Course Information:

  • Course Title: CSC-4240/5240: ARTIFICIAL INTELLIGENCE

  • Instructor: Amr Hilal

  • Date: 10/7/2025

Recap of First-Order Logic (FOL)

• Propositional Logic: Assumptions

  • Assumes the world contains facts.

• First-Order Logic (FOL): Assumptions

  • Assumes the world contains:

  • Objects:

    • Examples: people, houses, numbers, colors, baseball games, wars, etc.

  • Relations/Properties:

    • Examples: red, round, prime, brother, bigger than, part of, comes between, etc.

  • Properties: Unary relations such as red, round, etc.

  • Functions: Examples include father of, best friend, one more than, plus, etc.

• Construction of Facts: Facts in FOL are created by combining objects, properties, and functions.

More Examples of FOL

• All purple mushrooms are poisonous

  • Representation: $orall x (Purple(x) <br>ightarrow Poisonous(x))$

• A mushroom is poisonous if and only if it is purple

  • Representation: $orall x (Mushroom(x) <br>ightarrow Purple(x) <br>ightarrow Poisonous(x))$

• No purple mushroom is poisonous

  • Representation: $<br>eg( orall x (Purple(x) <br>ightarrow Mushroom(x) <br>ightarrow Poisonous(x)))$

• No human enjoys sushi

  • Representation: $orall x (Human(x) <br>ightarrow <br>eg Enjoys(x, Sushi))$

FOL Inference

• Recall, in Propositional Logic (PL):

  • Model checking and inference rules are applied.

  • Common rules: Modus Ponens, AND-elimination, AND/OR-Introduction, Resolution, etc.

• In FOL:

  • Focus on inference rules through two approaches:

  1. Reduction to Propositional Logic (Propositionalization):

     • Utilizes the existing knowledge of inference from propositional logic.

  2. Lifted Inference:

     • Seeks more general inference rules that are compatible with FOL.

Propositionalization

Step 1: Eliminate the Quantifiers

• Universal Instantiation (UI):

  • Proposes that every instantiation of a universally quantified sentence is entailed by it.

  • Representation: $orall v \beta ext{ Subst}( ext{{v/g}}, \beta)$

  • A variable $v$ can be substituted with any ground term $g$ making $\beta$ true.

  • Ground Term: A term absent of variables applicable to all objects in the Knowledge Base (KB).

  • Example:

    • From: $orall x (King(x) ext{ and } Greedy(x) <br>ightarrow Evil(x))$

    • Yields: $King(John) ext{ and } Greedy(John) <br>ightarrow Evil(John)$

    • Holds for: $King(Richard) ext{ and } Greedy(Richard) <br>ightarrow Evil(Richard)$

    • Provides: $King(Father(John)) ext{ and } Greedy(Father(John)) <br>ightarrow Evil(Father(John))$

    • From KB: $King(John), Person(Richard), orall x (King(x) <br>ightarrow Person(x))$

• Existential Instantiation (EI):

  • Replace an existentially quantified variable with a unique new constant symbol.

  • Representation: $orall v \beta ext{ Subst}( ext{{v/k}}, \beta)$

  • Example:

    • $orall x (Crown(x) ext{ and } OnHead(x, John))$ yields: $Crown(C1) ext{ and } OnHead(C1, John)$

    • Constant $C1$ is unique in the KB and permits substitution.

  • Notice: EI can only be applied once while UI can be repeatedly applied to replace the original quantifier.

Step 2: Reduce to Propositional Logic Syntax

• Convert predicates and functions into PL symbols:

  • Example Conversions:

    • $Pit(1,2) <br>ightarrow P_{1,2}$

    • $King(John) <br>ightarrow JohnIsKing$

    • $Brother(Richard, John) <br>ightarrow RichardIsBrotherOfJohn$

    • $Father(John) <br>ightarrow FatherOfJohn$

Example: Reduction to Propositional Inference

• FOL KB Given:

  • $orall x (King(x) ext{ and } Greedy(x) <br>ightarrow Evil(x))$

  • $King(John)$

  • $Greedy(John)$

  • $Brother(Richard, John)$

  • To ascertain if $Evil(John)$ can be inferred:

  • Instantiating the universal statement indicates:

    • From: $King(John) ext{ and } Greedy(John) <br>ightarrow Evil(John)$

    • Provides: $King(Richard) ext{ and } Greedy(Richard) <br>ightarrow Evil(Richard)$

    • New KB includes propositional symbols: $JohnIsKing, JohnIsGreedy, RichardIsKing, etc.$

  • Utilizes search algorithms to conclude $JohnIsEvil$ which is equivalent to $Evil(John)$.

Lifted Inference

Generalized Modus Ponens (GMP)

• Overview:

  • Propositionalization can create excessive instantiations of universally quantified sentences.

  • Rewrite PL inference rules to apply to FOL.

  • Generalization of Modus Ponens:

  • Lifts the Modus Ponens from propositional logic to first-order logic.

  • Inference rules transforming with a lifted approach.

Generalized Modus Ponens (GMP) Definition

• Notation:

  • Let $p<em>i, p</em>i', q$ be atomic sentences (Predicate(Term) or Term=Term).

  • $p_i, q$ include variables $v$.

  • $p_i'$ includes ground terms $g$ (which may include other variables).

  • Substitution Definition:

  • heta = ext{{v1/g1, v2/g2, v3/g3, …}} suggests replacing variables in $p<em>i$ with corresponding ground terms in $p</em>i'$ to conclude $q$.

Example for Generalized Modus Ponens

• Example KB:

  • $orall x (King(x) ext{ and } Greedy(x) <br>ightarrow Evil(x))$

  • $King(John)$

  • $orall y Greedy(y)$

  • $Brother(Richard, John)$

  • To deduce if $Evil(John)$ can still be inferred without propositionalization:

  • Set $p_i' = King(John)$

  • Set $p_i = King(x)$

  • Set $p_2' = Greedy(y)$

  • Set $p_2 = Greedy(x)$

  • Set $q = Evil(x)$

  • Define $heta$ as $heta = ext{{x/John, y/John}}$.

  • Apply substitution to arrive at $Evil(John)$.

Unification

• Definition:

  • Lifted inference methods necessitate discovering substitutions which render different logical expressions identical.

  • Immediate inference is possible when a substitution $heta$ is found such that $King(x)$ and $Greedy(x)$ match with $King(John)$ and $Greedy(y)$.

• Unify Algorithm:

  • Purpose: Takes two sentences and returns a unifier $heta$, or failure if one does not exist.

Unification Example

• Query: $AskVars(Knows(John, x))$ - identifies whom John knows.

• Output: Retrieval of answers by unifying with sentences in the KB that match $Knows(John, x)$:

  • Variables and sentences:

  • $p: Knows(John, x)$

  • $q: Knows(John, Jane)$

  • Unification results:

  • $heta = ext{{x/Jane}}$ making both sentences equivalent.

Examples of Further Unification

• Next Queries:

  • Other variables: $Knows(John, y), Knows(y, Biden), Knows(John, x), …$

  • Resulting substitutions yield varying outputs, e.g.:

  • Substitutions: {y/John, x/Biden}, etc.

Unify Algorithm Details

• Function UNIFY:

  • This function executes substitution to achieve identical expressions or recognize failure.

• Function Logic:

  • If both expressions are equivalent, return.

  • If one expression is a variable, it triggers another function UNIFY-VAR that performs specific checks.

  • If both are compound with arguments, or in a list format, it recursively unfolds their structured components until it finds a conclusion or a failure.

Most General Unification (MGU)

• Concept:

  • Unify expressions such as $Knows(John, x)$ and $Knows(y, z)$.

  • Potential substitutions: $θ = ext{{y/John, x/Jane, z/Jane}}$ or $θ = ext{{y/John, x/z}}$.

• Uniqueness of MGU:

  • There exists a unique most general unifier that remains valid through renaming of variables.

  • Example MGU is: $θ = {y/John, x/z}$, which is more general than the other substitution.

• Further Notes:

  • Check if a variable occurs within the term during matching to prevent unsound inference.

  • Adopted techniques may bypass this to simplify algorithm complexity.

Summary of Substitutions

• Example Unifications:

  • For various term pairs, list substitutions achieved or recognized failures in cases where terms match incorrectly, ensuring clear identification of successful and unsuccessful unifications.