AI · Knowledge, reasoning, and planning

9 · Inference in First-Order Logic

First-order rules can express general knowledge, but inference must discover which objects make those rules applicable. Follow a data-driven chain to a new conclusion.

How first-order inference works

9.1 Propositional vs. First-Order Inference

Propositional inference treats each sentence as a symbol. FOL inference must also find compatible substitutions for variables, so its search can be much larger or even nonterminating.

9.2 Unification and First-Order Inference

Unification finds substitutions that make expressions identical. For example, Parent(x, Ada) unifies with Parent(Lee, y) using {x/Lee, y/Ada}; incompatible constants cannot unify.

9.3 Forward Chaining

For definite clauses, repeatedly match rule premises against known facts and add the resulting conclusions. This is data-driven and reaches a fixed point when no fact is added.

9.4 Backward Chaining

Start from a query and recursively seek rules whose conclusions unify with it, then prove their premises. This goal-directed method is used in logic programming.

9.5 Resolution

Resolution refutation converts formulas to clauses and derives contradiction from a knowledge base plus the negated query. With FOL unification it is sound and refutation-complete for first-order logic.

Interactive forward chaining

Match, substitute, infer

Rules: Student(x) ∧ Studies(x) → Passes(x); Student(x) → Learner(x). Run one rule firing at a time.

Initial facts

    Rules applied

      Ready to derive consequences.

      Demo algorithm and complexity

      Let F be the maximum number of facts reached, R the number of rules, and A the total number of antecedent facts across the rules. A click scans for the first unused rule whose premises are all present, adds its conclusion, then redraws the fact/rule lists and checks the selected query.

      Time: O(R² + (A + R)·F) worst case per “Fire next rule” click: each rule can scan the used-rule list, premise checks scan facts, and a passing rule also checks whether its conclusion is already present. Across at most R firings plus one final no-match click, O(R³ + R·(A + R)·F) worst-case search work. Auxiliary/state space: O(F + R + A), including facts, fired-rule labels, and the rule set; the rendered lists use O(F + R) UI space. Here R = 2 and F ≤ 4. These bounds describe this simple finite ground-rule demo; general FOL inference has very different, potentially unbounded search costs.