Obsidian + 🪴 Quartz 4.0

AI - Lecture - First Order Logic Inference and Resolution

15 min read

AI - Lecture - First Order Logic Inference and Resolution

Introduction to Inference in FOL

Inference in First-Order Logic (FOL) is significantly more complex than in propositional logic due to several factors:

  • Variables and Quantifiers: The presence of and requires mechanisms to handle variable bindings.
  • Functions: These can generate infinitely many terms (e.g., ).
  • Substitutions: The necessity to match formulas by binding variables to specific terms.

Basic Strategy

The standard approach involves:

  1. Using Universal Instantiation and Existential Instantiation to remove quantifiers.
  2. Deriving sentences without quantifiers.
  3. Applying propositional-style inference to the resulting sentences.

Fundamental Properties

  • Completeness: FOL inference is complete; if , a proof procedure can eventually find .
  • Semi-decidability: If , the procedure may run forever.

Instantiation Rules

Universal Instantiation (UI)

From a universally quantified sentence , we can infer any instance obtained by replacing the variable with a ground term (a term containing no variables).

Rule: where

  • is the scope or logical formula that allows a quantifiers i.e. , is:
  • Substitution: A mapping from variables to terms, denoted as .
  • Logical Equivalence: The expanded Knowledge Base (KB) after UI is logically equivalent to the original.
  • Application: Can be applied multiple times to generate different instances.

Existential Instantiation (EI)

From an existentially quantified sentence , we infer a single instance by replacing with a new constant symbol .

Rule:

  • Skolem Constant: The new constant symbol must be “fresh” (not appearing elsewhere in the KB).
  • Inferential Equivalence: The new KB is not logically equivalent to the original, but it is inferentially equivalent for proving consequences.
  • Application: Applied only once to eliminate the existential sentence, which is then discarded.

Reduction to Propositional Inference

Propositionalization is the process of converting a FOL KB into a propositional KB.

Preprocessing Steps

  1. Eliminate Existential Quantifiers: Replace them with Skolem constants.
  2. Standardize Variables Apart: Rename variables in different sentences to avoid accidental clashes (e.g., and become and ).

The Process

  • Perform Universal Instantiation for all constants in the domain for every universal sentence.
  • Treat each ground atom (e.g., ) as a unique propositional symbol (e.g., ).

Limitations

  • Infinite Terms: If the KB contains function symbols, propositionalization may generate an infinite propositional KB (e.g., ).
  • Irrelevant Sentences: It often generates many ground sentences that are unnecessary for a specific proof, leading to inefficiency. For predicates of arity and constants, there can be up to ground atoms.

Herbrand’s Theorem

If a sentence is entailed by a first-order KB, then is entailed by some finite set of ground instances.

This suggests a semi-decision procedure:

  1. For depth :
  2. Generate ground instances up to depth .
  3. Apply propositional inference.
  4. Stop if .

Generalized Modus Ponens (GMP)

Generalized Modus Ponens “lifts” Modus Ponens from propositional logic to FOL by allowing premises to contain variables.

Formal Definition

If and are in the KB, and there exists a substitution such that for all , then we can infer:

Soundness

GMP is sound because:

  1. By Universal Instantiation (UI), the rule implies its instantiated version: .
  2. The matched facts provide the instantiated premises.
  3. follows by standard propositional Modus Ponens.

Unification

Unification is the process of finding a substitution that makes two first-order expressions identical.

  • Unifier: A substitution such that .
  • Most General Unifier (MGU): The substitution that imposes the fewest unnecessary constraints on variables.

Examples:

Expression 1Expression 2MGU ()
Failure (occurs-check)

Horn Clauses in FOL

GMP is primarily used with Horn clauses, which serve as the basis for Forward and Backward Chaining.

Definition: A Horn clause in FOL has the form: where and are non-negated atomic predicates.

  • Definite Clauses: Clauses with exactly one positive literal.
  • Negated Predicates: is equivalent to .

Forward Chaining in FOL

Forward Chaining is a data-driven strategy that repeatedly applies GMP to derive new facts until the query is solved or no new facts can be inferred.

Algorithmic Steps

function Forward-chaining(KB)
    local variable: new
    repeat
        new <- empty set
        for each sentence s = (p1 ^ ... ^ pn => q) in KB:
            for each theta such that Subst(theta, p1 ^ ... ^ pn) matches facts in KB:
                q' <- Subst(theta, q)
                if q' not in KB and q' not in new:
                    add q' to new
        add new to KB
    until new is empty
    return KB

Typical Use

  • When new observations are added to a KB.
  • To derive all possible consequences of known facts (e.g., in the Wumpus World).

Backward Chaining in FOL

Backward Chaining is a goal-driven procedure that starts from a query and works backwards through subgoals.

Algorithmic Steps

  1. Start with the query to prove.
  2. Find rules whose conclusion unifies with the query.
  3. Apply the unifier to the rule’s premises.
  4. Treat the premises as new subgoals.
  5. Recursively prove all subgoals.

Implementation Details

  • Propagation: Substitutions must be propagated to all subgoals.
  • Alternatives: If multiple rules unify with a goal, the algorithm tries different paths.
  • And-Or Graph: BC can be represented as an And-Or graph where the query succeeds if at least one chain of subgoals reaches known facts.

The “West” Knowledge Base Example

The following Horn clauses represent a scenario to prove Criminal(West):

Forward Chaining Proof

  • Iteration 1:
  • Iteration 2:

Backward Chaining Proof

  • Goal: Criminal(West)
    • Subgoals: American(West), Hostile(y), Weapon(z), Sells(West, y, z)
      • American(West) is a fact.
      • Hostile(Nono) unifies via Enemy(Nono, America).
      • Weapon(M) unifies via Missile(M).
      • Sells(West, Nono, M) unifies via Missile(M) and Owns(Nono, M).

Resolution

We saw in Propositional Logic > Resolution that propositional resolution is a complete inference procedure for propositional logic. In this section we extend it to first-order logic.

Conjunctive normal form for first-order logic

The first step is to convert sentences to conjunctive normal form (CNF).

In CNF, literals can contain variables, which are assumed to be universally quantified. For example, the sentence:

becomes in CNF:

The procedure for conversion to CNF is similar to the propositional case. The principal difference arises from the need to eliminate existential quantifiers.

For example, translating the sentence “Everyone who loves all animals is loved by someone” or:

The steps are the following:

  1. Eliminate implications
  2. Move inwards
  3. Standardize variables
  4. Skolemize: remove existential quantifiers
  5. Drop universal quantifiers
  6. Distribute over

First, eliminate implications by replacing with . For our sentence this must be done 2 times:

Second, move negation inwards. In addition to the usual rules for negated connectives, we need rules for negated quantifiers thus we have:

  • becomes
  • becomes

Our sentence goes through the following transformations:

Notice how a universal quantifier () in the premise of the implication has become an existential quantifier. The sentence now reads “Either there is some animal that doesn’t love, or (if this is not the case) someone loves x.” Clearly, the meaning of the original sentence has been preserved.

Then we have to standardize variables: for sentences like: that use the same variable name twice, change the name of one of the variables. This avoids confusion later when we drop the quantifiers. Thus, we have

Next step is skolemization that is the process of removing existential quantifers by elimination.

If we blindly apply the rule to the two matching parts we get:

which has the wrong meaning entirely: it says that everyone either fails to love a particular animal A or is loved by some particular entity B.

In fact, our original sentence allows each person to fail to love a different animal or to be loved by a different person. Thus, we want the Skolem entities to depend on x: Where and are Skolem functions.

The general rule is that the arguments of the Skolem function are all the universally quantified variables in whose scope the existential quantifier appears. As with Existential Instantiation, the Skolemized sentence is satisfiable exactly when the original sentence is satisfiable.

Drop universal quantifiers: At this point, all remaining variables must be universally quantified. Therefore, we don’t lose any information if we drop the quantifier: Finally, distribute over :

This step may also require flattening out nested conjunctions and disjunctions.

The sentence is now in CNF and consists of two clauses.

The resolution inference rule

The resolution rule for first-order clauses is simply a lifted version of the propositional resolution rule.

Two clauses, which are assumed to be standardized apart so that they share no variables, can be resolved if they contain complementary literals.

Propositional literals are complementary if one is the negation of the other; first-order literals are complementary if one unifies with the negation of the other.

Thus, we have:

  • where

Example: and becomes

This rule is called the binary resolution rule because it resolves exactly two literals. However, this binary resolution rule does not yield a complete inference procedure. The full resolution rule resolves subsets of literals in each clause that are unifiable.

Example Proofs

Resolution proves that by proving that is unsatisfiable, that is by deriving the empty clause. The algorithmic approach is identical to the propositional case.

Consider the crime example: We also include the negated goal ¬Criminal(West)

The resolution proof is shown in the following figure (9.10):

Our second example make us of Skolemization and involves clauses that are not definite clauses.

Consider this riddle:

Everyone who loves all animals is loved by someone. Anyone who kills an animal is loved by no one. Jack loves all animals. Either Jack or Curiosity killed the cat, who is named Tuna. Did Curiosity kill the cat?

First, we express the original sentences, some background knowledge, and the negated goal G in first-order logic:

  • A.
  • B.
  • C.
  • D.
  • E.
  • F.
  • G.

Now we apply the conversion procedure to convert each sentence to CNF:

  • A1.
  • A2.
  • B.
  • C.
  • D.
  • E.
  • F.
  • G.

The resolution proof that Curiosity killed the cat is given in Figure 9.11. :

Unfortunately, resolution can sometimes produce nonconstructive proofs for existential goals, where we know a query is true, but there isn’t a unique binding for the variable.

Godel’s incompleteness theorem

Kurt Godel was able to show, in his incompleteness theorem, that there are true arithmetic sentences that cannot be proved. The proof of the incompleteness theorem is somewhat beyond the scope of this note as it occupies atleast 30 pages.

We can give an hint there.

Conside the logical theory of numbers, where there is a single constant 0 and a single function (the successor function).

In the intended model, S(0) denotes 1, S(S(0)) denotes 2, and so on; the language therefore has names for all the natural numbers.

The vocabulary also includes the function symbols +, ×, and Expt (exponentiation) and the usual set of logical connectives and quantifiers.

The first step is to notice that the set of sentences that we can write in this language can be enumerated. We can then number each sentence α with a unique natural number (the Godel number ).

This is crucial: number theory contains a name for each of its own sentences. Similarly, we can number each possible proof P with a Godel number G(P), because a proof is simply a finite sequence of sentences.

Now suppose we have a recursively enumerable set A of sentences that are true statements about the natural numbers. Recalling that A can be named by a given set of integers, we can imagine writing in our language a sentence of the following sort: , is not the Godel number of a proof of the sentence whose Godel number is , where the proof uses only premises in A.

Then let σ be the sentence that is, a sentence that states its own unprovability from A. (That this sentence always exists is true but not entirely obvious.)

Now we make the following ingenious argument: Suppose that σ is provable from A; then is false because says it cannot be proved. But then we have a false sentence that is provable from A, so A cannot consist of only true sentences— a violation of our premise. Therefore, σ is not provable from A. But this is exactly what σ itself claims; hence σ is a true sentence.

So in summary, for any set of true sentences of number theory, and in particular any set of basic axioms, there are other true sentences that cannot be proved from those axioms. This establishes, among other things, that we can never prove all the theorems of mathematics within any given system of axioms.

Application of FC, BC and Resolution

Forward Chaining:

  • Encoding condition-action rules to recommend actions, based on a data-driven approach
  • Production systems (production: condition-action rules)
  • Expert systems

Backward Chaining:

  • Logic programming languages (e.g. Prolog), used for
  • Rapid prototyping
  • Symbol processing applications (compilers, NL parsers, …)

Resolution:

  • Main application → theorem provers, used for
    • Assisting mathematicians
    • Proof checking
    • Verification and synthesis of hardware and software

Cluedo Puzzle Solving by FOL Resolution

In this exercise we will solve a simplified Cluedo puzzle using:

  • First order logic to represent suspects, weapons, rooms and clues.

Then we need to convert everything to CNF because we want to use resolutions.

Then we apply the resolution inference to derive contradictions to prove what must be true.

Goal: determine “Who commited the murder, with which weapon, and in which room”.

Mystery Setting

A crime was committed by:

  • one of the three suspects: scarlet, mustard, plum
  • With one of the three weapons: knife, revolver, candlestick
  • On three rooms: library, kitchen, ballroom

We have general assumptions:

  • The person in the crime room is the murderer
  • the weapon found in the crime room is the murder weapon.

Goal: Determine the murderer, the weapon and the room.

The first goal is knowledge engineer. In this game we use the constants in the mystery setting. It is common to use lowercase in order to avoid confusion with predicates.

FOL Predicates:

  • Person x was in room r
  • is the murdeer
  • s the murderer weapon
  • The crime happened in room …
  • found the weapon in room

Solving Process:

  1. FOL Translation of Clues
  2. Conversion to CNF
  3. Resolution Proof: Crime Room
  4. Resolution Proof: Murderer
  5. Resolution Proof: Weapon
  6. Final Solution

FOL Translation facts

From scenario:

  • At(scarlett, library)
  • At(plum, kitchen)
  • At(mustard, ballroom)
  • Found(revolver, kitchen)
  • Found(knife, library)
  • Found(candlestick, ballroom)
  • CrimeRoom(library)

Mustard was not in the same room as the crime:

The person in the crime room is the murderer

The weapon found in the crime room is the murder weapon:

At least one room is the crime room:

Uniqueness constraints We assume that the solution contains:

  • exactly one crime room
  • exactly one murderer
  • exactly one murder weapon

The following caluses do not necessarily all appear in the final poof, but they are part of the complete logical model of the Cluedo puzzle.

At most one room is the crime room:

Transforming Clauses in CNF:

So Mustard was not in the same room as the crime becomes:

The person in the crime room is the murderer becomes:

The weapon found in the crime room is the murder weapon becomes:

Atleast one roome is the crime room stays the same:

Now we have the 11 facts (CNF Clauses):

Resolution Proof: The Crime Room

Prove: CrimeRoom(kitchen)

we prove it by contradiction.

Add the negated query:

For readibility let , for crime room library and for ballroom:

We consider clause 12:

We combine C9 and C3 to infer: C13: and from C8 so we can infer that: C14:

Then apply C7 and C14, to remove library C15:

and we can combine it with that we wanted to prove by contradiction to get the (), that is abasurd i.e unsatisfiable. this mean that the original goal is entailed so CrimeRoom(kitchen)

C3 C9
 \ / 
  C13 C8
   \ /
    C14 C7
     \ / 
      C15

Now we know the crime room.

Now we have to prove the murderer: Murderer(plum).

So we add the negated query C17:

relevant clauses are C2 and C10 and we can follow a similar process to get the and the negated of murderer.

Then resolution proof: the weapon, we prove MurdererWeapon(revolver), add the negated query C21, relevant clauses are C4, C16, C(11)

C22:

Resolve C22 with C4 to get: therefore C23: and to get C24: that can be simplifed with C17 to get () and so we find also the weapon.

Note: we had to add some modelling assumptions: the person in the crime room, then this person is the murderer, and if we find a weapon in a crimeroom then that weapon is used to kill. If we do not had these two sentences we can prove only that but not the other facts.

Because being in the crime room doesnot logically imply being guily unless we explicitly model that assumption.

Graph View

Backlinks