First-order logic and knowledge representation

Propositional logic forced us to write the breeze rule separately for every square of the wumpus world. That is because it can talk only about facts, not about objects and their relations. First-order logic (FOL), also called predicate logic, adds objects, relations, functions, variables and quantifiers, so one sentence can say 'every square next to a pit is breezy' or 'every course's prerequisites must be completed first'. It is expressive enough to formalize most of mathematics and much everyday knowledge, and it is the foundation of logic programming, databases and the ontologies that organize knowledge on the web.

This lesson covers the syntax and semantics of FOL, how to translate English into it, the inference methods that lift propositional techniques to first-order sentences (unification, forward chaining, backward chaining and resolution), and the broader question of knowledge representation: how to organize a large body of knowledge about categories, objects and their properties using ontologies, semantic networks and description logics. CMPUT-272 covered predicate logic as mathematics, and CMPUT-325 builds a Prolog interpreter; here the focus is on representation and reasoning for agents.

Syntax and semantics

The basic elements of first-order logic are constant symbols that name objects (Ana, Edmonton, Cmput366), predicate symbols that name relations (Prereq, Adjacent, Pit), and function symbols that map objects to objects (MotherOf, Capital). A term refers to an object: a constant, a variable, or a function applied to terms, such as Capital(Alberta). An atomic sentence applies a predicate to terms, such as Prereq(Cmput366, Cmput204), and complex sentences combine atomic ones with the connectives of propositional logic.

Quantifiers let us talk about collections of objects. The universal quantifier ∀x P(x) says that P holds for every object, and the existential quantifier ∃x P(x) says that P holds for at least one. Equality, written t1 = t2, says that two terms refer to the same object. The semantics of FOL is given by models consisting of a domain (a non-empty set of objects) and an interpretation that maps each constant to an object, each predicate to a relation over the domain and each function to a function on it. A sentence is true in a model if the relations hold as the sentence claims; entailment is defined, as before, as truth in every model of the knowledge base.

Two translation rules prevent most beginner errors. The natural connective under ∀ is ⇒: '∀x Student(x) ⇒ Smart(x)' says all students are smart, while '∀x Student(x) ∧ Smart(x)' says that everything in the universe is a smart student. The natural connective under ∃ is ∧: '∃x Student(x) ∧ Smart(x)' says some student is smart, while '∃x Student(x) ⇒ Smart(x)' is true as soon as anything at all is not a student. Quantifier order also matters: ∀x ∃y Loves(x, y) says everyone loves somebody, and ∃y ∀x Loves(x, y) says there is somebody whom everyone loves.

Knowledge engineering

Building a knowledge base is called knowledge engineering. The process has a standard shape. Identify the questions the knowledge base must answer. Assemble the relevant knowledge, often by interviewing experts. Decide on a vocabulary of predicates, functions and constants; this choice, the ontology of the domain, is the most consequential decision. Encode general knowledge as axioms, encode the specific problem instance as facts, pose queries to an inference procedure, and debug the knowledge base when answers are wrong. Debugging a knowledge base resembles debugging a program, except that the bug is usually a missing or overly general axiom rather than a wrong line of code.

For the wumpus world, the vocabulary might include Adjacent(s1, s2), Pit(s), Breezy(s) and At(agent, s, t), with time as an argument so that changing facts can be represented. Then a handful of sentences replace the dozens of propositional ones: ∀s Breezy(s) ⇔ ∃r Adjacent(r, s) ∧ Pit(r). The same pattern of general axioms plus specific facts appears in every knowledge-based system, from tax rules to configuration of telephone networks.

From propositional to first-order inference

One way to do first-order inference is to reduce it to propositional inference. Universal instantiation replaces a universally quantified variable with any ground term: from ∀x King(x) ⇒ Evil(x) we can infer King(John) ⇒ Evil(John). Existential instantiation replaces an existentially quantified variable with a new constant symbol, a Skolem constant. Propositionalizing a whole knowledge base this way works but is wasteful, because it instantiates rules with every object, relevant or not, and with function symbols there are infinitely many ground terms. In fact, entailment in first-order logic is semidecidable: a procedure exists that says yes to every entailed sentence, but no procedure can always say no to non-entailed ones.

The efficient alternative is to apply inference rules to sentences with variables directly. Generalized modus ponens says: from P1′, …, Pn′ and (P1 ∧ … ∧ Pn ⇒ Q), infer Subst(θ, Q), where θ is a substitution that makes each Pi′ identical to Pi. Finding θ is the job of unification.

Unification

Unification takes two expressions and finds a substitution that makes them identical, if one exists. UNIFY(Knows(Ana, x), Knows(Ana, Raj)) gives {x/Raj}. UNIFY(Knows(Ana, x), Knows(y, Mother(y))) gives {y/Ana, x/Mother(Ana)}. UNIFY(Knows(Ana, x), Knows(x, Lee)) fails, because x cannot be both Ana and Lee; standardizing apart, renaming the variables of one sentence so they do not clash, avoids such spurious failures when the two x's are really different variables. When unification succeeds there is a most general unifier (MGU), unique up to renaming of variables, that commits to as little as possible.

# Unification for first-order terms. Variables are strings starting with an uppercase letter;
# compound terms are tuples (functor, arg1, ...); constants are lowercase strings.
def is_var(t): return isinstance(t, str) and t[:1].isupper()

def walk(t, s):
    while is_var(t) and t in s: t = s[t]
    return t

def occurs(v, t, s):
    t = walk(t, s)
    return t == v or (isinstance(t, tuple) and any(occurs(v, a, s) for a in t[1:]))

def unify(a, b, s=None):
    """Return the most general unifier extending s, or None if a and b cannot be unified."""
    s = {} if s is None else s
    a, b = walk(a, s), walk(b, s)
    if a == b: return s
    if is_var(a): return None if occurs(a, b, s) else {**s, a: b}
    if is_var(b): return None if occurs(b, a, s) else {**s, b: a}
    if isinstance(a, tuple) and isinstance(b, tuple) and a[0] == b[0] and len(a) == len(b):
        for x, y in zip(a[1:], b[1:]):
            s = unify(x, y, s)
            if s is None: return None
        return s
    return None

def resolve(t, s):
    t = walk(t, s)
    return (t[0],) + tuple(resolve(a, s) for a in t[1:]) if isinstance(t, tuple) else t

def show(t): return t if not isinstance(t, tuple) else f"{t[0]}({', '.join(map(show, t[1:]))})"

cases = [
    (("knows", "ana", "X"),             ("knows", "ana", "raj")),
    (("knows", "ana", "X"),             ("knows", "Y", ("mother", "Y"))),
    (("knows", "ana", "X"),             ("knows", "X", "lee")),
    (("knows", "ana", "X"),             ("knows", "Y", "Y")),
    (("f", "X", ("g", "X")),            ("f", ("h", "Z"), "W")),
    (("loves", "X", "X"),               ("loves", "Y", ("parent", "Y"))),
]
for a, b in cases:
    s = unify(a, b)
    if s is None: print(f"{show(a):18} and {show(b):24} fail")
    else:
        mgu = {v: show(resolve(v, s)) for v in sorted(s)}
        print(f"{show(a):18} and {show(b):24} unify with {mgu}")

knows(ana, X)      and knows(ana, raj)          unify with {'X': 'raj'}
knows(ana, X)      and knows(Y, mother(Y))      unify with {'X': 'mother(ana)', 'Y': 'ana'}
knows(ana, X)      and knows(X, lee)            fail
knows(ana, X)      and knows(Y, Y)              unify with {'X': 'ana', 'Y': 'ana'}
f(X, g(X))         and f(h(Z), W)               unify with {'W': 'g(h(Z))', 'X': 'h(Z)'}
loves(X, X)        and loves(Y, parent(Y))      fail

The last case fails because of the occurs check: unifying X with parent(X) would require an infinite term. The check makes unification sound but costs time proportional to the size of the term, so Prolog, for efficiency, omits it by default. With a good indexing scheme, unification is fast enough to run millions of times a second, and it is the core operation of every first-order reasoner.

Forward and backward chaining

First-order definite clauses are universally quantified implications whose premises and conclusion are atoms, such as ∀c ∀q ∀p Prereq(c, q) ∧ Requires(q, p) ⇒ Requires(c, p). Forward chaining works as in lesson 7, except that rules fire for every substitution that matches known facts. When there are no function symbols, the knowledge base is a Datalog program, and forward chaining reaches a fixed point after a polynomial number of steps: there are only finitely many ground facts that can be built from the constants. Deductive databases and many program analysis tools are Datalog engines.

Backward chaining starts from a query with variables and finds all substitutions that prove it. To prove Requires(cmput204, X), it unifies the goal with each rule head (after renaming the rule's variables) and recursively proves the rule body, depth first. This procedure, SLD resolution, is exactly how Prolog executes programs. The program below states a few prerequisite facts modeled on this university's computing courses, and the rule that requires is the transitive closure of prereq.

# Forward and backward chaining with first-order definite clauses over course prerequisites.
import itertools
def is_var(t): return isinstance(t, str) and t[:1].isupper()
def walk(t, s):
    while is_var(t) and t in s: t = s[t]
    return t
def unify(a, b, s):
    a, b = walk(a, s), walk(b, s)
    if a == b: return s
    if is_var(a): return {**s, a: b}
    if is_var(b): return {**s, b: a}
    if isinstance(a, tuple) and isinstance(b, tuple) and len(a) == len(b):
        for x, y in zip(a, b):
            s = unify(x, y, s)
            if s is None: return None
        return s
    return None
def subst(t, s): return tuple(walk(x, s) for x in t)

FACTS = [("prereq", "cmput366", "cmput204"), ("prereq", "cmput366", "stat151"),
         ("prereq", "cmput204", "cmput201"), ("prereq", "cmput204", "cmput272"),
         ("prereq", "cmput201", "cmput174"), ("prereq", "cmput272", "cmput174"),
         ("prereq", "cmput367", "cmput204"), ("prereq", "cmput367", "math125")]
RULES = [  # (head, body): head holds whenever every body atom holds
    (("requires", "C", "P"), [("prereq", "C", "P")]),
    (("requires", "C", "P"), [("prereq", "C", "Q"), ("requires", "Q", "P")]),
    (("shared", "A", "B", "P"), [("requires", "A", "P"), ("requires", "B", "P")]),
]

def forward_chain(facts, rules):
    known, rounds = set(facts), 0
    while True:
        rounds += 1; new = set()
        for head, body in rules:
            def match(i, s):                         # join the body atoms against known facts
                if i == len(body): yield s; return
                for f in sorted(known):
                    s2 = unify(body[i], f, s)
                    if s2 is not None: yield from match(i + 1, s2)
            for s in match(0, {}):
                fact = subst(head, s)
                if fact not in known: new.add(fact)
        if not new: return known, rounds
        known |= new

known, rounds = forward_chain(FACTS, RULES)
reqs = sorted(f[2] for f in known if f[:2] == ("requires", "cmput366"))
print(f"forward chaining reached a fixed point after {rounds} rounds with {len(known)} facts")
print("cmput366 requires, directly or indirectly:", ", ".join(reqs))
print("shared by cmput366 and cmput367:", ", ".join(sorted(f[3] for f in known if f[:3] == ("shared", "cmput366", "cmput367") )))

counter = itertools.count()
def rename(rule):                                     # fresh variables for every use of a rule
    n = next(counter); r = lambda t: tuple(f"{x}_{n}" if is_var(x) else x for x in t)
    head, body = rule
    return r(head), [r(b) for b in body]

def backward_chain(goals, s, depth=0):
    """Yield every substitution that proves all goals (SLD resolution, depth first)."""
    if not goals: yield s; return
    first, rest = goals[0], goals[1:]
    for f in FACTS:
        s2 = unify(first, f, s)
        if s2 is not None: yield from backward_chain(rest, s2, depth + 1)
    for rule in RULES:
        head, body = rename(rule)
        s2 = unify(first, head, s)
        if s2 is not None: yield from backward_chain(body + rest, s2, depth + 1)

answers = sorted({walk("X", s) for s in backward_chain([("requires", "cmput204", "X")], {})})
print("backward chaining, requires(cmput204, X):", answers)
print("backward chaining, requires(stat151, X):", sorted({walk("X", s) for s in backward_chain([("requires", "stat151", "X")], {})}) or "no answers")

forward chaining reached a fixed point after 5 rounds with 72 facts
cmput366 requires, directly or indirectly: cmput174, cmput201, cmput204, cmput272, stat151
shared by cmput366 and cmput367: cmput174, cmput201, cmput204, cmput272
backward chaining, requires(cmput204, X): ['cmput174', 'cmput201', 'cmput272']
backward chaining, requires(stat151, X): no answers

Forward chaining derives every consequence, 72 facts in all, including many no query will ask about; backward chaining computes only the answers for its query. Backward chaining has its own hazards. Depth-first search can loop on left-recursive rules such as Requires(c, p) ⇐ Requires(c, q) ∧ Prereq(q, p), and it can re-derive the same subgoal many times. Prolog programmers order clauses and goals carefully to avoid this, and tabling (memoizing subgoals, as in XSB Prolog) fixes it systematically. CMPUT-325 implements Prolog's unification and SLD resolution in detail.

For full first-order logic, beyond definite clauses, resolution remains complete. Sentences are converted to clausal form by eliminating implications, moving negations inward, standardizing variables apart, Skolemizing (replacing ∃y inside ∀x with a Skolem function F(x)), dropping universal quantifiers and distributing ∨ over ∧. The resolution rule then applies to clauses whose complementary literals unify. Resolution-based theorem provers such as Vampire and E prove theorems in mathematics and verify software and hardware; interactive proof assistants like Lean and Isabelle combine human guidance with automated steps.

Ontologies and categories

Larger knowledge bases need structure beyond individual axioms. An ontology is a formal specification of the concepts of a domain and the relations among them. An upper ontology provides the most general concepts, such as physical objects, events, time intervals, places and measures, under which domain ontologies attach their specific concepts. Much reasoning is about categories: Courses, Birds, Provinces. Categories can be represented as predicates (Bird(x)) or reified as objects (Birds), which lets us state facts about the category itself, such as Population(Birds) or Disjoint({Birds, Mammals}).

Categories form a taxonomy through subclass relations: Penguins ⊂ Birds ⊂ Animals. Membership and subclass relations support inheritance: if all birds have feathers, and penguins are birds, then penguins have feathers. Other useful relations include disjointness (no object is both a bird and a mammal), exhaustive decomposition (every animal is a vertebrate or an invertebrate), and partition (both). Physical composition is captured by a PartOf relation, which is transitive: a keyboard is part of a laptop, which is part of a lab.

Semantic networks and frames

Semantic networks, introduced in the 1960s, draw knowledge as a graph: nodes for categories and objects, and labeled links for relations, with special links for membership and subclass. They make inheritance easy to compute by following links upward, and they are easy for people to read. Frames, proposed by Marvin Minsky in 1975, organize knowledge around objects with slots and fillers, including default values that can be overridden. Both were early attempts to make knowledge representation efficient and natural, and both live on in object-oriented programming and in modern knowledge graphs.

# A semantic network with inheritance and default values that more specific nodes can override.
NET = {
    "animal":       {"isa": None,     "props": {"alive": True, "breathes": True}},
    "bird":         {"isa": "animal", "props": {"has_feathers": True, "flies": True, "legs": 2}},
    "penguin":      {"isa": "bird",   "props": {"flies": False, "swims": True}},
    "goose":        {"isa": "bird",   "props": {"migrates": True}},
    "mammal":       {"isa": "animal", "props": {"has_fur": True, "legs": 4}},
    "bat":          {"isa": "mammal", "props": {"flies": True, "legs": 2}},
    "pingu":        {"isa": "penguin", "props": {"lives_in": "a zoo"}},
    "honker":       {"isa": "goose",   "props": {"injured_wing": True, "flies": False}},
}

def lookup(node, prop):
    """Walk up the isa links; the first (most specific) value found wins."""
    path = []
    while node is not None:
        path.append(node)
        if prop in NET[node]["props"]: return NET[node]["props"][prop], " -> ".join(path)
        node = NET[node]["isa"]
    return None, " -> ".join(path)

for node, prop in [("pingu", "flies"), ("pingu", "has_feathers"), ("pingu", "breathes"),
                   ("honker", "migrates"), ("honker", "flies"), ("bat", "flies"), ("bat", "legs"), ("bat", "swims")]:
    value, path = lookup(node, prop)
    if value is None: print(f"{node:7} {prop:13} unknown (searched {path})")
    else: print(f"{node:7} {prop:13} = {str(value):6} found by {path}")

pingu   flies         = False  found by pingu -> penguin
pingu   has_feathers  = True   found by pingu -> penguin -> bird
pingu   breathes      = True   found by pingu -> penguin -> bird -> animal
honker  migrates      = True   found by honker -> goose
honker  flies         = False  found by honker
bat     flies         = True   found by bat
bat     legs          = 2      found by bat
bat     swims         unknown (searched bat -> mammal -> animal)

The program shows inheritance with exceptions. Birds fly by default, but the penguin node overrides that, and an individual goose with an injured wing overrides it again. Bats are mammals but fly. This style of reasoning is nonmonotonic: learning a new fact (Honker has an injured wing) can retract a previous conclusion (Honker flies), which never happens in classical logic, where adding axioms only adds conclusions. Nonmonotonic logics, such as default logic and circumscription, formalize this. A related idea is the closed-world assumption used by databases and Prolog: anything not known to be true is taken to be false. Our backward chainer answered 'no answers' for requires(stat151, X) because no prerequisite of STAT-151 was recorded, not because it was proved that none exists.

Description logics

Description logics are families of logics designed to make reasoning about categories decidable and efficient. They describe concepts by combining simpler ones: Student ⊓ ∃takes.AICourse means 'students who take some AI course', and Course ⊓ ∀prereq.Introductory means 'courses all of whose prerequisites are introductory'. The principal inference tasks are subsumption (is every member of one concept necessarily a member of another?) and classification (where does a new concept fit in the taxonomy?). By restricting what can be said, description logics guarantee that these questions are decidable, unlike full first-order logic, and their complexity has been mapped precisely.

The Web Ontology Language (OWL), a W3C standard, is based on description logics, and reasoners such as HermiT check large OWL ontologies for consistency and compute their taxonomies. SNOMED CT, the clinical terminology used in health records in Canada, the United States and many other countries, contains several hundred thousand concepts organized by a description logic. Knowledge graphs such as Wikidata store billions of simple facts as subject–relation–object triples with lighter-weight schemas. Search engines, digital assistants and question-answering systems draw on them, and current research combines them with large language models, which can generate fluent text but do not by themselves guarantee consistency or provenance of facts.

Worked examples