Logic & Knowledge Representation

Propositional logic is the simplest formal system for reasoning about truth. It deals with atomic propositions (indivisible statements that are either true or false) combined by logical connectives.

Syntax defines what counts as a well-formed formula (WFF):

• Atomic propositions: P, Q, Raining, DoorOpen
• ¬φ (negation: "not φ")
• φ ∧ ψ (conjunction: "φ and ψ")
• φ ∨ ψ (disjunction: "φ or ψ")
• φ → ψ (implication: "if φ then ψ")
• φ ↔ ψ (biconditional: "φ if and only if ψ")

Semantics defines what formulas mean via a model — an assignment of truth values to all atomic propositions. A formula is:

• satisfiable if at least one model makes it true
• valid (a tautology) if every model makes it true
• unsatisfiable (a contradiction) if no model makes it true

The fundamental tool for checking semantics is the truth table. For n propositions there are 2^n rows — this exponential blowup is not accidental; propositional satisfiability (SAT) is NP-complete.

A crucial semantic concept is logical entailment: KB ⊨ α means that in every model where the knowledge base KB is true, α is also true. Entailment is what we want from a reasoning system — it captures the idea that α "follows from" KB with absolute certainty.

The connectives have standard precedence: ¬ binds tightest, then ∧, then ∨, then →, then ↔. So ¬P ∧ Q → R parses as (¬P ∧ Q) → R.

# Truth-table enumeration for a propositional formula
from itertools import product

def evaluate(formula, model):
    """formula: callable(model) -> bool"""
    return formula(model)

def truth_table(props, formula):
    print(*props, 'result')
    for vals in product([False, True], repeat=len(props)):
        model = dict(zip(props, vals))
        result = formula(model)
        print(*[int(v) for v in vals], int(result))

# Example: (P → Q) ↔ (¬P ∨ Q)
def f(m):
    P, Q = m['P'], m['Q']
    implies  = (not P) or Q        # P → Q
    equiv    = implies == ((not P) or Q)   # biconditional
    return equiv

truth_table(['P', 'Q'], f)
# All rows produce True — this is a tautology

A knowledge base (KB) is a set of sentences (formulas) that an agent believes to be true about the world. An inference procedure derives new sentences from the KB.

Two essential properties of any inference procedure:

• Soundness: every sentence derived is actually entailed by KB. (We never derive falsehoods from truths.) Formally: if KB ⊢ α then KB ⊨ α.
• Completeness: every sentence entailed by KB can eventually be derived. Formally: if KB ⊨ α then KB ⊢ α.

A sound but incomplete procedure is safe but may miss conclusions. A complete but unsound procedure may derive wrong conclusions. We want both — and for propositional logic, such procedures exist.

Modus Ponens is the simplest sound inference rule:

  α → β,  α
  ---------
       β

"If it rains, the street gets wet. It is raining. Therefore the street is wet."

Forward chaining starts from known facts and applies Modus Ponens repeatedly until the goal is derived or no new facts can be added. It is data-driven.

Backward chaining starts from the goal and works backwards, asking what premises would suffice. It is goal-driven and is how Prolog executes queries.

The model-checking approach to inference enumerates all models and checks whether α is true in all models where KB is true — correct but exponential. For practical AI we need smarter approaches.

# Forward chaining on a propositional Horn KB
# Horn clause: at most one positive literal (A ∧ B → C)

def forward_chain(clauses, facts):
    """
    clauses: list of (premises_set, conclusion)
    facts:   set of known true atoms
    Returns the closure of all derivable facts.
    """
    changed = True
    known = set(facts)
    while changed:
        changed = False
        for premises, conclusion in clauses:
            if premises.issubset(known) and conclusion not in known:
                known.add(conclusion)
                changed = True
    return known

# KB: Raining ∧ HasUmbrella → StayDry
#     Raining → RoadWet
rules = [
    ({'Raining', 'HasUmbrella'}, 'StayDry'),
    ({'Raining'},                'RoadWet'),
]
print(forward_chain(rules, {'Raining', 'HasUmbrella'}))
# {'Raining', 'HasUmbrella', 'StayDry', 'RoadWet'}

Conjunctive Normal Form (CNF) is a canonical form for propositional formulas: a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals (atoms or their negations).

Example: (P ∨ ¬Q) ∧ (¬P ∨ R ∨ S) ∧ (¬R)

Every propositional formula can be converted to CNF (though the size may increase exponentially in the worst case; the Tseitin transformation gives a linear-size CNF equisatisfiable formula by introducing fresh variables).

The Resolution Rule operates on two CNF clauses that contain complementary literals:

  (A ∨ ... ∨ P)   (¬P ∨ B ∨ ...)
  --------------------------------
         (A ∨ ... ∨ B ∨ ...)

You resolve on P: if P is false then the first clause forces A ∨ ...; if P is true then the second clause forces B ∨ .... Either way, A ∨ ... ∨ B ∨ ... must be true.

Resolution Refutation: to prove KB ⊨ α, add ¬α to KB (converted to CNF) and apply resolution until the empty clause (□) is derived. Deriving □ means we reached a contradiction — so ¬α must be false when KB is true, i.e., α must be true. This is proof by contradiction.

The Resolution Theorem (Robinson, 1965): Resolution is sound and complete for propositional logic. Any unsatisfiable set of CNF clauses can be refuted by resolution.

The main challenge is the search strategy: which pairs of clauses to resolve? Naive approaches are exponential. Strategies like unit propagation (always resolve unit clauses first), pure literal elimination, and DPLL/CDCL make SAT solvers practical on millions of variables.

def resolve(ci, cj):
    """
    ci, cj: frozensets of literals (strings; negation = '~X')
    Returns set of all resolvents, or None if no complementary pair.
    """
    resolvents = []
    for lit in ci:
        neg = lit[1:] if lit.startswith('~') else '~' + lit
        if neg in cj:
            resolvent = (ci - {lit}) | (cj - {neg})
            resolvents.append(frozenset(resolvent))
    return resolvents

def resolution_refutation(clauses):
    """Return True if clause set is unsatisfiable."""
    clauses = set(clauses)
    while True:
        new = set()
        pairs = [(ci, cj) for ci in clauses for cj in clauses if ci != cj]
        for ci, cj in pairs:
            for r in resolve(ci, cj):
                if len(r) == 0:          # empty clause!
                    return True
                new.add(r)
        if new.issubset(clauses):
            return False                 # saturated, satisfiable
        clauses |= new

# Prove: {P, P→Q} ⊨ Q
# KB ∧ ¬Q = {P} ∧ {¬P ∨ Q} ∧ {¬Q}
clauses = [
    frozenset({'P'}),
    frozenset({'~P', 'Q'}),
    frozenset({'~Q'}),          # negated goal
]
print(resolution_refutation(clauses))   # True

Propositional logic cannot talk about objects and their relationships. "Every student who studies hard passes" cannot be expressed propositionally without enumerating every student. First-Order Logic (FOL), also called predicate logic, adds the machinery for this.

New syntactic elements beyond propositional logic:

1. Constants: specific objects — Alice, 3, London.
2. Variables: placeholders for objects — x, y, z. (Lowercase by convention in AI.)
3. Function symbols: map objects to objects — father(x), plus(x, y). Functions applied to terms yield terms.
4. Predicate symbols: map objects to truth values — Loves(Alice, Bob), Prime(x), GreaterThan(x, y).
5. Quantifiers:
   • Universal: ∀x P(x) — "for all x, P(x) is true"
   • Existential: ∃x P(x) — "there exists some x such that P(x) is true"

A term is either a constant, variable, or function applied to terms. An atomic formula (atom) is a predicate applied to terms. Complex formulas are built from atoms using connectives and quantifiers.

Scope and binding: In ∀x (Student(x) → ∃y Teaches(y, x)), the x in Student(x) and Teaches(y, x) is bound by ∀x. A variable not bound by any quantifier is free. A formula with no free variables is a sentence — it has a definite truth value.

Key equivalences (De Morgan for quantifiers):

• ¬∀x P(x) ≡ ∃x ¬P(x) (not all birds fly ≡ some bird doesn't fly)
• ¬∃x P(x) ≡ ∀x ¬P(x) (no bird flies ≡ every bird doesn't fly)

# There is no "run this" for FOL syntax per se, but we can
# represent FOL sentences as Python data structures — as a
# simple logical form parser/AST.

# Represent: ∀x (Student(x) → ∃y (Professor(y) ∧ Teaches(y,x)))
# "Every student is taught by some professor."

ForAll = lambda var, body: ('forall', var, body)
Exists = lambda var, body: ('exists', var, body)
Implies = lambda a, b:     ('implies', a, b)
And     = lambda a, b:     ('and', a, b)
Atom    = lambda pred, *args: (pred,) + args

sentence = ForAll('x',
    Implies(
        Atom('Student', 'x'),
        Exists('y',
            And(
                Atom('Professor', 'y'),
                Atom('Teaches', 'y', 'x')
            )
        )
    )
)
print(sentence)
# ('forall', 'x', ('implies', ('Student', 'x'),
#   ('exists', 'y', ('and', ('Professor', 'y'), ('Teaches', 'y', 'x')))))

FOL semantics requires specifying what the symbols mean. A model (or interpretation) M = ⟨D, I⟩ consists of:

• Domain D: a non-empty set of objects (the "universe of discourse")
• Interpretation I: maps constants to elements of D, function symbols to functions D^n → D, and predicate symbols to relations D^n → {T, F}

Under model M:

• ∀x φ(x) is true iff for every element d ∈ D, φ(d) is true
• ∃x φ(x) is true iff for some element d ∈ D, φ(d) is true

Entailment KB ⊨ α means: in every model that satisfies KB, α is also satisfied.

The Unique Names Assumption (UNA): in databases and many AI systems, different constant names denote different objects. FOL itself does not assume this — Alice and Bob might refer to the same person.

The Closed World Assumption (CWA): if a fact is not provable from the KB, assume it is false. Databases use CWA. Open-world reasoning (OWA), used in ontologies, instead says: unprovable facts are unknown, not false. This distinction is crucial in practice.

Herbrand Models: for theorem proving, it is sufficient to consider models whose domain consists exactly of the ground terms constructable from the KB's constants and functions. Herbrand's theorem says: a set of FOL clauses is unsatisfiable iff it is unsatisfiable on a Herbrand model — grounding the abstract problem to propositional-like reasoning.

# Small model checker for ground FOL (no variables)
# Domain: {alice, bob, carol}
# Predicates: Likes, Happy

domain = {'alice', 'bob', 'carol'}
Likes  = {('alice','bob'), ('bob','carol'), ('alice','carol')}
Happy  = {'bob'}

def forall(domain, pred):
    return all(pred(d) for d in domain)

def exists(domain, pred):
    return any(pred(d) for d in domain)

# ∀x ∃y Likes(x, y)  — every person likes someone
sentence1 = forall(domain, lambda x:
                exists(domain, lambda y: (x, y) in Likes))
print('Every person likes someone:', sentence1)   # False (carol likes nobody)

# ∃x Happy(x)  — someone is happy
sentence2 = exists(domain, lambda x: x in Happy)
print('Someone is happy:', sentence2)             # True (bob)

Unification is the process of finding a substitution that makes two expressions syntactically identical. It is the computational heart of FOL inference — without it, you cannot apply general rules to specific cases.

A substitution θ is a mapping from variables to terms: {x/Alice, y/father(Bob)}. Applying θ to an expression replaces each variable with its mapped term. Loves(x, y)θ = Loves(Alice, father(Bob)).

The Most General Unifier (MGU) is the least committed substitution that unifies two expressions. It is unique up to variable renaming and is computable in near-linear time (Paterson & Wegman 1978).

Unification algorithm (Robinson, 1965):

1. If both are the same constant/variable, return the identity substitution.
2. If one is a variable x not occurring in the other term t, return {x/t}.
3. If one is a variable x occurring in t (the occur check), fail — no unifier exists (would create circular substitution).
4. If both are compound f(t₁,...,tₙ) and f(s₁,...,sₙ), unify each pair of arguments left-to-right, composing substitutions.
5. Otherwise (different functors/arities), fail.

Example: Unify Knows(John, x) with Knows(y, Jane):

• Unify John with y → {y/John}
• Unify x with Jane → {x/Jane}
• MGU: {y/John, x/Jane}
• Result: Knows(John, Jane)

Note: Prolog typically omits the occur check for efficiency, which can cause infinite loops on pathological inputs but is safe on well-behaved programs.

def unify(x, y, subst={}):
    """Return MGU of x and y given existing subst, or None on failure.
    Terms: strings (constants/variables start with lowercase),
           or tuples (functor, arg1, ...) for compound terms.
    Variables start with uppercase for clarity here."""
    if subst is None:
        return None
    elif x == y:
        return subst
    elif is_variable(x):
        return unify_var(x, y, subst)
    elif is_variable(y):
        return unify_var(y, x, subst)
    elif isinstance(x, tuple) and isinstance(y, tuple):
        if x[0] != y[0] or len(x) != len(y):
            return None
        s = subst
        for xi, yi in zip(x[1:], y[1:]):
            s = unify(xi, yi, s)
        return s
    return None

def is_variable(x): return isinstance(x, str) and x[0].isupper()

def unify_var(var, x, subst):
    if var in subst:   return unify(subst[var], x, subst)
    if x in subst:     return unify(var, subst[x], subst)
    if occurs(var, x): return None          # occur check
    return {**subst, var: x}

def occurs(var, x):
    if var == x: return True
    if isinstance(x, tuple): return any(occurs(var, t) for t in x[1:])
    return False

# Unify Knows(John, X) with Knows(Y, Jane)
result = unify(('Knows','john','X'), ('Knows','Y','jane'))
print(result)  # {'X': 'jane', 'Y': 'john'}

Propositional resolution extends naturally to FOL. The key insight is to convert FOL formulas to Skolem Normal Form (SNF) / Clausal Form, then apply resolution with unification.

Converting FOL to Clausal Form (step by step):

1. Eliminate biconditionals and implications
2. Move negations inward (using De Morgan and quantifier duality)
3. Standardize variables apart (rename so each quantifier uses a unique variable)
4. Skolemize (eliminate existential quantifiers): replace ∃y P(y) with a Skolem constant c; replace ∀x ∃y P(x,y) with a Skolem function f(x) — the idea is that the witness y depends on x.
5. Drop universal quantifiers (all remaining variables are universally quantified implicitly)
6. Distribute ∨ over ∧ to get CNF clauses.

FOL Resolution Rule: Given clauses C₁ (containing literal L₁) and C₂ (containing literal ¬L₂):

• If L₁ and L₂ unify with MGU θ
• Resolvent is (C₁ - {L₁}) ∪ (C₂ - {¬L₂}) all under substitution θ

Completeness: Gödel's Completeness Theorem (1929) establishes that FOL has a complete proof system — if KB ⊨ α, there is a finite proof. Robinson (1965) showed resolution specifically is complete for refutation.

But: FOL is only semi-decidable. If KB ⊨ α, the resolution procedure will eventually terminate and confirm it. But if KB ⊭ α, the procedure might loop forever — you can never be sure you've searched long enough. This is the price of FOL's expressiveness, captured by Church's undecidability theorem.

# Skolemization example (by hand, shown in pseudocode)

# Original: ∀x (Student(x) → ∃y (Professor(y) ∧ Teaches(y, x)))
# Step 1 - eliminate →:
# ∀x (¬Student(x) ∨ ∃y (Professor(y) ∧ Teaches(y, x)))
# Step 2 - negation already innermost
# Step 3 - variables already standardized
# Step 4 - Skolemize ∃y (depends on x) → Skolem function advisor(x):
# ∀x (¬Student(x) ∨ (Professor(advisor(x)) ∧ Teaches(advisor(x), x)))
# Step 5 - drop ∀:
# (¬Student(x) ∨ (Professor(advisor(x)) ∧ Teaches(advisor(x), x)))
# Step 6 - distribute ∨ over ∧ (CNF):
# Clause 1: {¬Student(x), Professor(advisor(x))}
# Clause 2: {¬Student(x), Teaches(advisor(x), x)}

# Now add the fact: Student(Alice)
# Clause 3: {Student(alice)}

# Resolve Clause 1 with Clause 3: unify Student(x) with Student(alice) -> x/alice
# Resolvent: {Professor(advisor(alice))}  <-- derived!
# Resolve Clause 2 with Clause 3:
# Resolvent: {Teaches(advisor(alice), alice)}  <-- derived!
# We have proven: Professor(advisor(alice)) ∧ Teaches(advisor(alice), alice)

Prolog (PROgramming in LOGic) is a programming language where programs ARE knowledge bases written in a restricted subset of FOL called definite clauses (Horn clauses with exactly one positive literal), and execution IS proof search via resolution.

A Prolog program consists of:

• Facts: parent(tom, bob). — "Tom is a parent of Bob"
• Rules: ancestor(X, Y) :- parent(X, Y). — "X is an ancestor of Y if X is a parent of Y" ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y). — recursive case
• Queries: ?- ancestor(tom, ann). — "Is Tom an ancestor of Ann?"

Prolog's execution model:

1. To prove a goal G, find a clause whose head unifies with G.
2. Replace G with the body of that clause (substituting the MGU).
3. Prove each subgoal left-to-right, depth-first.
4. Backtrack when a subgoal fails — try the next matching clause.

This is essentially SLD resolution (Selective Linear Definite resolution) — a complete strategy for Horn clauses.

Prolog's cut operator ! prunes the search tree: once past a cut, backtracking cannot undo choices made before it. This gives efficiency but sacrifices completeness — it's a pragmatic concession.

Prolog has been used for natural language parsing (DCG grammars), expert systems, type inference in compilers, and constraint programming. Its limitation: the depth-first search can loop on left-recursive rules, and it is not complete for full FOL (only Horn clauses).

% Family knowledge base in Prolog
parent(tom,  bob).
parent(tom,  liz).
parent(bob,  ann).
parent(bob,  pat).

% Base case: parent is an ancestor
ancestor(X, Y) :- parent(X, Y).

% Recursive case: ancestor through chain
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

% Query: ?- ancestor(tom, ann).
% Execution trace:
%   Try ancestor(tom, ann) via rule 1: parent(tom, ann)? FAIL
%   Backtrack, try rule 2: parent(tom, Z), ancestor(Z, ann)
%     parent(tom, bob) succeeds, Z=bob
%     ancestor(bob, ann) via rule 1: parent(bob, ann)? SUCCEED
% Result: true

% List membership (classic recursive definition)
member(X, [X|_]).             % X is head of list
member(X, [_|T]) :- member(X, T).  % X is in tail

% ?- member(b, [a,b,c]).   => true
% ?- member(X, [1,2,3]).   => X=1 ; X=2 ; X=3 (via backtracking)

Real-world AI knowledge bases need more than bare FOL. Several important representation frameworks have been developed:

Ontologies and Description Logics: An ontology formalizes the concepts and relationships in a domain. Description Logics (DL) are decidable fragments of FOL, forming the basis for OWL (Web Ontology Language). DLs let you say:

• Doctor ⊑ Person (every doctor is a person — subsumption)
• Doctor ⊑ ∀treats.Patient (doctors treat only patients)
• ¬(Doctor ⊓ Patient) (no one is both a doctor and a patient)

The key insight: DLs trade expressiveness for decidability — the subsumption and instance-checking problems are decidable, enabling guaranteed correct reasoning over ontologies.

Frame Systems and Semantic Networks: Pre-FOL representations that organized knowledge as nodes (concepts) and links (relations). Modern knowledge graphs (Freebase, Wikidata, Google Knowledge Graph) are essentially semantic networks. They lack formal inference but scale to billions of triples.

Non-Monotonic Reasoning: Classical logic is monotonic — adding new facts can never invalidate old conclusions. But real-world reasoning is often default reasoning: "birds fly" with exceptions (penguins). Systems like default logic (Reiter 1980) and circumscription (McCarthy 1980) allow conclusions that can be retracted when new information arrives.

The Frame Problem (McCarthy & Hayes 1969): In a changing world, how do you represent that most things stay the same when an action occurs? If you push a block, the block moves — but your coffee cup, the weather, and the laws of physics don't change. Explicitly asserting all non-changes leads to an explosion of "frame axioms". This deep problem motivated the development of situation calculus and later STRIPS/PDDL for planning.

# Simplified Description Logic subsumption check
# Concepts as Python sets (extensional semantics over a finite domain)

Person   = {'alice', 'bob', 'carol', 'dave'}
Doctor   = {'alice', 'bob'}          # Alice and Bob are doctors
Patient  = {'carol', 'dave', 'bob'}  # Carol, Dave, Bob are patients

def is_subsumed(A, B):
    """A ⊑ B: every instance of A is also an instance of B?"""
    return A.issubset(B)

print('Doctor ⊑ Person:', is_subsumed(Doctor, Person))    # True
print('Doctor ⊑ Patient:', is_subsumed(Doctor, Patient))  # False (alice)
print('Doctor ⊓ Patient = ∅:', Doctor & Patient == set()) # False (bob)

# Default reasoning: birds fly, except penguins
birds    = {'tweety', 'sam', 'opus'}
penguins = {'opus'}   # penguins are birds that don't fly

flies = {b for b in birds if b not in penguins}  # default rule with exception
print('Flies:', flies)   # {'tweety', 'sam'}

Modern automated reasoning goes far beyond classroom resolution. SAT solvers and SMT solvers are industrial-strength tools used daily in hardware verification, software model checking, and formal proofs.

DPLL (Davis–Putnam–Logemann–Loveland, 1962): The classic complete SAT algorithm.

1. Unit propagation: if a clause has only one unset literal, it must be true.
2. Pure literal elimination: if a literal appears only positively, set it true.
3. Decision: pick an unset variable, guess a value, recurse.
4. Backtrack on conflict.

CDCL (Conflict-Driven Clause Learning): Modern extension that learns new clauses from conflicts, dramatically pruning the search. Tools like MiniSAT, Z3, and CaDiCaL can handle SAT instances with millions of variables in seconds.

SMT (Satisfiability Modulo Theories): Extends SAT with theories about arithmetic, arrays, bitvectors, strings, etc. Z3 (Microsoft) and CVC5 decide whether formulas like x > 0 ∧ y > 0 ∧ x + y < 1 ∧ x = 2y have a solution. SMT solvers underlie:

• Program verification (Dafny, Frama-C)
• Symbolic execution (KLEE, angr)
• Hardware verification (Cadence, Synopsys flows)

Interactive theorem provers (Coq, Lean 4, Isabelle) combine logic, dependent types, and human-guided proof construction to certify mathematical theorems and software correctness to the highest possible standard. The Flyspeck project formally verified Hales' proof of the Kepler conjecture (14 years of work; ~300 pages of dense math) entirely in HOL Light.

# Using Python's z3 bindings (pip install z3-solver)
from z3 import *

# Can we satisfy: x > 0, y > 0, x + y < 1, x = 2*y?
x, y = Reals('x y')
solver = Solver()
solver.add(x > 0, y > 0, x + y < 1, x == 2*y)

if solver.check() == sat:
    m = solver.model()
    print(f"x = {m[x]}, y = {m[y]}")
    # x = 2/3, y = 1/3  (example satisfying assignment)
else:
    print('unsatisfiable')

# SMT for program verification:
# Prove that for all integers n >= 0, n*(n+1) is always even
n = Int('n')
s = Solver()
# Try to FIND a counterexample (negation of claim)
s.add(n >= 0, (n * (n + 1)) % 2 != 0)
print(s.check())  # unsat => no counterexample => claim proven

Understanding the limits is as important as understanding the capabilities.

Decidability: A logic is decidable if there is an algorithm that terminates on all inputs and correctly determines satisfiability.

• Propositional logic: decidable (but NP-complete)
• FOL: undecidable (Church 1936, Turing 1936) — no algorithm can decide satisfiability in general
• FOL is semi-decidable: if a formula is unsatisfiable, the algorithm may loop forever instead of saying "no"
• Many fragments are decidable: Datalog (function-free FOL with only existential queries), DL-Lite, monadic FOL, etc.

Tractability: Even decidable logics can be intractable:

• Propositional satisfiability: NP-complete
• Propositional model counting: #P-complete
• Description logic reasoning: ranges from P to EXPTIME depending on the logic

The Qualification Problem: Preconditions for actions are never fully specified. "Start the car" requires: key in ignition, fuel, working engine, battery not dead, not underwater, not in space... The list is open-ended. FOL cannot handle this elegantly without an infinite axiom set.

The Frame Problem: Tracking what changes (and what does not) after an action requires either infinite "non-change" axioms, or clever representational tricks (situation calculus with the successor state axiom, PDDL's STRIPS assumption that everything not in the effect list stays the same).

Common-Sense Reasoning: Human knowledge is vast, uncertain, contextual, and inconsistently defined. CYC (Doug Lenat, 1984–present) attempted to encode all common-sense knowledge in FOL — tens of millions of assertions — and found that the scale of knowledge required made pure logic impractical without massive human curation.

These limits motivated the rise of probabilistic methods (Bayesian networks, Markov logic networks), deep learning, and ultimately the neurosymbolic hybrid approaches active in research today.

# Demonstration: even small FOL KB can require exponential search
# The pigeonhole principle is hard for resolution:
# n+1 pigeons into n holes => some hole has 2 pigeons
# This has exponential-size shortest resolution proofs (Ben-Sasson & Wigderson 1999)

# Propositionally encode: 3 pigeons, 2 holes (pigeon[i][j] = pigeon i in hole j)
# At least one hole per pigeon:
# (p00 ∨ p01) ∧ (p10 ∨ p11) ∧ (p20 ∨ p21)
# At most one pigeon per hole (pairwise exclusion):
# ¬p00 ∨ ¬p10, ¬p00 ∨ ¬p20, ¬p10 ∨ ¬p20  (hole 0)
# ¬p01 ∨ ¬p11, ¬p01 ∨ ¬p21, ¬p11 ∨ ¬p21  (hole 1)
# This is UNSATISFIABLE but has no short resolution proof
# — illustrating that resolution completeness != efficiency

print("The pigeonhole principle requires exponential-length")
print("resolution proofs -- provably no polynomial shortcut exists.")
print("This is why CDCL clause learning was revolutionary:")
print("learned clauses allow SAT solvers to escape this trap.")