Logical Agents

Propositional and first-order logic, entailment, inference, unification, rule systems, symbolic planning, and the limits of representing a changing world with explicit facts.

Search treats states as structures that an algorithm can generate and compare. Knowledge-based agents need something more expressive: a language for describing facts, relations, rules, and conclusions. Knowledge representation asks what should be made explicit and which inferences should follow from it.

Logic provides a contract between syntax and meaning. A knowledge base contains sentences in a formal language; an inference procedure derives new sentences; semantics determines whether those conclusions are justified.

Logic Basics

Syntax specifies well-formed expressions.
Semantics assigns truth conditions to expressions.
A knowledge base KB entails sentence α, written KB ⊨ α, when every model satisfying KB also satisfies α.

Entailment is a property of meaning. Inference, written KB ⊢ᵢ α, is a computational process carried out by procedure i.

An inference procedure is:

sound if it derives only entailed conclusions;
complete if it can derive every entailed conclusion.

A fast procedure may be sound but incomplete. A complete procedure may be computationally expensive.

Propositional Logic

Propositional logic uses atomic propositions and connectives:

negation ¬P;
conjunction P ∧ Q;
disjunction P ∨ Q;
implication P → Q;
biconditional P ↔ Q.

Suppose:

Power       the room has power
Network     the network is available
Service     the service is reachable

Rules:

Power ∧ Network → Service
¬Power → ¬Service

A model assigns truth values to all propositions. Model checking can test whether every model of the knowledge base also satisfies a query. It is conceptually simple but exponential in the number of symbols.

from itertools import product

def entails(symbols, knowledge_base, query):
    names = tuple(symbols)

    for values in product((False, True), repeat=len(names)):
        model = dict(zip(names, values))
        if knowledge_base(model) and not query(model):
            return False

    return True

symbols = ("Power", "Network", "Service")

def knowledge_base(model):
    power = model["Power"]
    network = model["Network"]
    service = model["Service"]
    rule = not (power and network) or service
    return power and network and rule

def service_query(model):
    return model["Service"]

assert entails(symbols, knowledge_base, service_query)

An implication P → Q is implemented as ¬P ∨ Q. Model checking is deliberately exhaustive and therefore suitable only for small symbol sets, but it gives a semantic reference against which a faster inference method can be tested.

Implication and Causation

P → Q says that no allowed model has P true and Q false. It does not by itself say that P causes Q, occurs earlier, or provides an explanation.

The converse Q → P also does not follow. If rain implies wet ground, wet ground does not prove rain; sprinklers remain possible.

Resolution

A formula is in conjunctive normal form (CNF) when it is a conjunction of clauses, each a disjunction of literals:

(A ∨ ¬B) ∧ (C ∨ D) ∧ (¬A ∨ C)

Resolution combines:

A ∨ X
¬A ∨ Y
---------
X ∨ Y

To prove KB ⊨ α, resolution uses contradiction:

convert KB ∧ ¬α to CNF;
repeatedly resolve clauses;
if the empty clause is derived, the assumptions are inconsistent, so α is entailed.

Resolution is sound and complete for propositional logic, but naive resolution can generate many irrelevant clauses.

Resolution Example

Suppose the knowledge base contains:

Network → Service
Service → Portal
Network

To prove Portal, add ¬Portal and convert implications:

¬Network ∨ Service
¬Service ∨ Portal
Network
¬Portal

Resolve ¬Service ∨ Portal with ¬Portal to obtain ¬Service. Resolve that with ¬Network ∨ Service to obtain ¬Network. Resolving ¬Network with Network yields the empty clause.

The proof is refutational: it establishes that the knowledge base together with denial of the query has no model. A resolution engine should record parent clauses so the empty clause can be expanded into an auditable proof.

Horn Rules

A definite Horn rule has one positive conclusion:

Premise₁ ∧ Premise₂ ∧ ... → Conclusion

Forward chaining begins with known facts and fires rules whose premises are satisfied:

def forward_chain(facts, rules):
    known = set(facts)
    changed = True

    while changed:
        changed = False
        for premises, conclusion in rules:
            if premises <= known and conclusion not in known:
                known.add(conclusion)
                changed = True

    return known

This is data-driven: new facts trigger consequences. It suits monitoring and configuration.

A useful engine should also explain each derived fact:

def forward_chain_with_proof(facts, rules):
    known = set(facts)
    proof = {fact: ("given", ()) for fact in facts}

    changed = True
    while changed:
        changed = False
        for premises, conclusion in rules:
            if premises <= known and conclusion not in known:
                known.add(conclusion)
                proof[conclusion] = (
                    "rule", tuple(sorted(premises))
                )
                changed = True

    return known, proof

rules = [
    ({"Power", "Network"}, "Service"),
    ({"Service"}, "Portal"),
]
known, proof = forward_chain_with_proof(
    {"Power", "Network"}, rules
)
assert "Portal" in known
assert proof["Service"] == ("rule", ("Network", "Power"))

The proof map records immediate justification, not merely the final truth value. Following its premise links yields an explanation tree. In a changing system, those links also identify conclusions that must be reconsidered when a supporting fact is retracted.

Backward chaining begins with a query and asks which rules could establish it, recursively proving their premises. It is goal-driven and avoids unrelated consequences, but requires cycle detection and careful handling of repeated subgoals.

First-Order Logic

Propositional logic needs a separate symbol for every fact. First-order logic (FOL) represents objects, properties, relations, and quantified rules.

Components include:

constants: lab1, sabbir;
variables: x, room;
predicates: Teaches(person, course);
functions: SupervisorOf(student);
universal quantifier ∀;
existential quantifier ∃.

Example:

∀x Lecturer(x) → Employee(x)
Lecturer(Sabbir)

Therefore:

Employee(Sabbir)

An existential statement:

∃x Student(x) ∧ NeedsSupport(x)

says at least one such student exists without naming one.

Quantifier Order

∀x ∃y Helps(y, x)

Everyone is helped by someone, possibly a different person.

∃y ∀x Helps(y, x)

One person helps everyone. The formulas are not equivalent.

Unification

Inference in FOL requires matching expressions through substitutions. Unification finds a substitution making two expressions identical.

Teaches(x, AI)
Teaches(Sabbir, y)

unify with:

{x/Sabbir, y/AI}

Unification must reject inconsistent substitutions and self-referential terms. It is the mechanism behind many logic programming and rule engines.

The occurs check prevents substitutions such as {x / Parent(x)}, which would require an infinite term. Some practical logic languages omit this check for speed, changing the formal behavior of unification. Such implementation choices belong in the system’s specification.

Inference Control

Logical validity does not determine which rule to try first. An inference engine still needs control:

indexes from predicates to relevant rules;
an agenda of newly added facts;
memoization of completed subgoals;
cycle detection;
variable standardization so separate rule uses do not collide;
limits for recursion, time, or generated clauses.

A naive forward chainer repeatedly scans every rule, as the teaching implementation does. A production version stores a count of unmet premises and places newly enabled rules on an agenda. This changes efficiency without changing which Horn consequences are derived.

Backward chaining faces a dual choice. It focuses on one query but may revisit the same failed subgoal through many rules. Tabling stores subgoal results, turning some exponential recursive searches into manageable graph computations.

Retraction

Ordinary Horn inference is monotonic: new premises only add conclusions. A changing agent also needs retraction. If Service was derived from Power and Network, losing Power may invalidate Service and everything supported only by it.

A truth-maintenance system stores justifications and distinguishes assumptions from derived facts. When a premise disappears, it retracts conclusions with no remaining support. If another independent rule still supports the same conclusion, that conclusion remains.

This is why the proof map is operationally useful, not only explanatory. Reasoning over time requires dependencies between beliefs, not a flat set of strings.

Logic Limits

Classical logic is exact, but real knowledge may be incomplete, inconsistent, uncertain, vague, or time-dependent. A valid proof can still rest on a false premise. Logical entailment also does not assign confidence or rank competing explanations.

Inference can be expensive. Propositional satisfiability is NP-complete, and unrestricted first-order entailment is only semidecidable. Practical agents restrict languages, use indexes, prefer Horn rules, or combine symbolic inference with search and probability.

Applications

rule engines;
theorem proving;
access control;
configuration;
program analysis;
query systems;
symbolic diagnosis.

Common Mistakes

Reversing an implication.
Treating absence as false without stating a closed-world assumption.
Confusing validity with truth of premises.
Writing rules whose variables are not quantified clearly.
Ignoring cycles in backward chaining.
Calling a plausible conclusion logically entailed.

Exercises

Translate five access-control requirements into propositional logic.
Convert an implication into CNF and perform a resolution step.
Extend forward chaining to record each conclusion’s justification.
Write quantified statements for courses, students, and instructors.
Give two formulas whose meaning changes with quantifier order.
Unify several predicate pairs and identify one impossible pair.
Compare model checking with forward chaining on a Horn knowledge base.
Extend the proof map to produce a nested explanation for a query.
Give an occurs-check failure and explain the infinite term it implies.