First-Order Logic: Objects, Relations, Quantifiers and Unification

Propositional logic treats the world as a list of facts. But the world has structure: it contains objects (students, courses, cities), relations between them (enrolled-in, adjacent-to) and functions (the lecturer of a course). First-order logic (FOL), also called predicate logic, captures that structure and is the most important knowledge-representation language in classical AI.

Syntax of FOL#

FOL adds the following building blocks:

• Constants name specific objects: Janin, AUST, CSE101.
• Predicates express properties and relations: Student(x), Enrolled(x, c).
• Functions map objects to objects: Lecturer(CSE101).
• Variables: $x, y, z$.
• Quantifiers: universal $\forall$ ("for all") and existential $\exists$ ("there exists").
• Equality: $=$.

Examples:

Two classic mistakes#

Quantifier order matters too: $\forall x\, \exists y\; \text{Loves}(x, y)$ ("everyone loves someone") is very different from $\exists y\, \forall x\; \text{Loves}(x, y)$ ("there is someone whom everyone loves").

The quantifiers are dual: $\forall x\; \neg P(x) \equiv \neg \exists x\; P(x)$.

Semantics#

A model in FOL contains a domain of objects and an interpretation mapping constants to objects, predicates to relations and functions to functions. Because domains may be infinite, we can no longer check entailment by enumerating models — we need proof procedures.

Knowledge engineering#

Writing a good knowledge base is a craft. The process is:

1. Identify the task and the questions the KB must answer.
2. Assemble relevant knowledge (interview experts).
3. Decide on a vocabulary of predicates, functions and constants — an ontology.
4. Encode general knowledge as axioms.
5. Encode the specific problem instance.
6. Pose queries and debug.

Unification#

Inference in FOL requires matching sentences that contain variables. Unification finds a substitution $\theta$ that makes two expressions identical:

We always want the most general unifier (MGU) — the one that commits to the fewest bindings.

def unify(x, y, theta):
    """Terms: variables are strings starting with '?', compound terms are tuples."""
    if theta is None:
        return None
    if x == y:
        return theta
    if isinstance(x, str) and x.startswith("?"):
        return unify_var(x, y, theta)
    if isinstance(y, str) and y.startswith("?"):
        return unify_var(y, x, theta)
    if isinstance(x, tuple) and isinstance(y, tuple) and len(x) == len(y):
        for a, b in zip(x, y):
            theta = unify(a, b, theta)
        return theta
    return None

def unify_var(v, t, theta):
    if v in theta:
        return unify(theta[v], t, theta)
    if isinstance(t, str) and t in theta:
        return unify(v, theta[t], theta)
    if occurs(v, t, theta):
        return None                       # occurs check prevents x = f(x)
    return {**theta, v: t}

def occurs(v, t, theta):
    if v == t:
        return True
    if isinstance(t, str) and t in theta:
        return occurs(v, theta[t], theta)
    return isinstance(t, tuple) and any(occurs(v, a, theta) for a in t)

print(unify(("Knows", "John", "?x"), ("Knows", "?y", ("Mother", "?y")), {}))

Generalised Modus Ponens#

With unification, modus ponens lifts to FOL: from $p_1', \dots, p_n'$ and $(p_1 \land \dots \land p_n \Rightarrow q)$, if a substitution $\theta$ makes each $p_i'\theta = p_i\theta$, infer $q\theta$. This powers forward chaining (used in production systems and databases) and backward chaining (used in Prolog).

parent(tom, bob).
parent(bob, ann).
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).
% ?- grandparent(tom, Who).   ->  Who = ann

Resolution for FOL#

For full FOL, we convert sentences to clausal form. Two new steps appear:

• Skolemisation removes existential quantifiers: $\forall x\, \exists y\; \text{Loves}(x, y)$ becomes $\text{Loves}(x, F(x))$, where $F$ is a new Skolem function.
• Dropping universal quantifiers, since all remaining variables are implicitly universal.

Resolution with unification is refutation-complete: if $KB \models \alpha$, it will eventually derive a contradiction from $KB \land \neg\alpha$. However, FOL entailment is only semi-decidable — if $\alpha$ is not entailed, the procedure may run forever. This is a deep consequence of Gödel's and Turing's work.