Logical Agents and Planning

A knowledge-based agent acts on a description of its world. Its knowledge base (KB) contains formal sentences: initial facts and rules, called axioms, and information added during operation. Inference connects those sentences to conclusions the agent has never directly observed.

Connect perception to action

TELL adds a sentence to the KB. ASK requests an answer supported by it, either already stored or derived. At each time step the agent records its percept, asks what action to take, records the chosen action, and executes it. Recording actions matters because later reasoning needs to know how the world has changed.

At the knowledge level, we might say that a robot knows a passage is blocked and wants to reach a storage area. At the implementation level, we describe data structures and inference procedures. A declarative design supplies facts and rules; a procedural design writes behavior directly in code. A working agent can combine them.

Read the wumpus world

The wumpus world is a 4 × 4 grid. Coordinates are [column, row]; the agent starts at [1, 1] facing right. There is one wumpus, one piece of gold, and a pit probability of 0.2 in each square except the start. Pits and the wumpus stay put. The world is discrete, deterministic and single-agent, but partially observable: the layout is hidden.

A Breeze signals a pit in a directly adjacent square; a Stench signals the wumpus there. Diagonal squares do not count. Glitter marks gold in the current square, Bump reports a wall, and Scream reports the wumpus's death anywhere in the cave. Actions are Forward, TurnLeft, TurnRight, Grab, Shoot and Climb. The agent has one arrow; Climb exits only from [1, 1]. Leaving with gold earns 1000 points, dying loses 1000, every action costs 1, and shooting costs another 10.

Combine observations

At [1, 1], no Breeze rules out pits at [1, 2] and [2, 1]; no Stench rules out the wumpus there. Both squares are safe. At [2, 1], a Breeze puts a pit in [2, 2] or [3, 1], because the start has none. No Stench rules out the wumpus in [2, 2] and [3, 1].

The agent next visits [1, 2]. No Breeze excludes a pit at [2, 2], so the earlier disjunction forces a pit at [3, 1]. A Stench at [1, 2] locates the wumpus in [1, 3] or [2, 2]. The earlier no-Stench observation excludes [2, 2], leaving [1, 3]. The agent has established that [2, 2] contains neither hazard without entering it.

This reasoning depends on both the percepts and the rules linking percepts to hazards. An unexplored square is unknown when the KB supports neither safety nor danger. Failure to derive danger is insufficient for a claim of safety. Choosing to enter such a square requires a decision about risk, beyond the entailments alone.

Propositional logic gives an agent precise rules for combining yes-or-no claims. An atomic symbol names a whole claim, such as P₁₂ for "there is a pit in [1, 2]." A literal is an atom or its negation. Larger sentences combine them with ¬, ∧, ∨, ⇒ and ⇔.

Evaluate the connectives

A model assigns true or false to each symbol. With n symbols there are 2ⁿ assignments. Negation reverses a truth value; a conjunction needs both sides true; inclusive disjunction needs at least one. An implication is false only with a true premise and a false conclusion. A biconditional needs equal truth values on both sides.

The binding order is ¬, ∧, ∨, ⇒, ⇔. Thus ¬A ∧ B ⇒ C means ((¬A) ∧ B) ⇒ C. Use parentheses when the intended grouping might be unclear. With A true, B false and C true, (A ∨ B) ⇒ C is true, while A ⇒ (B ∧ C) is false.

Logical implication states a constraint on truth values, not a cause. A false premise makes the implication true. It also gives no license to reverse the direction: from "if the battery is empty, the robot stops," stopping alone cannot establish an empty battery.

Encode both directions of a rule

The breeze rule at the start is B₁₁ ⇔ (P₁₂ ∨ P₂₁). It says a breeze occurs exactly when a neighboring pit exists. The direction B₁₁ ⇒ (P₁₂ ∨ P₂₁) supports hazard detection from a breeze. The reverse direction supports pit exclusion from no breeze. Omitting it loses the inference from ¬B₁₁ to ¬P₁₂ ∧ ¬P₂₁.

Each square needs its own propositional rule. Encoding exactly one wumpus among 16 squares needs an at-least-one disjunction plus an at-most-one constraint for each pair. There are 16 × 15 / 2 = 120 distinct pairs. Propositional symbols cannot quantify over squares, so general rules become many separate sentences.

Represent change without losing persistence

A fluent is a fact whose truth can change. A time superscript distinguishes its values: L₁₁⁰ records location at time 0. An effect axiom can say that moving right from [1, 1] produces location [2, 1] at time 1 and removes the old location. It leaves open what happens to unrelated facts, such as possession of the arrow. Describing all these unchanged facts is the frame problem.

A successor-state axiom gives one complete update rule per fluent: Fᵗ⁺¹ ⇔ (an action makes F true) ∨ (Fᵗ ∧ no action makes F false). For the arrow, HaveArrowᵗ⁺¹ ⇔ (HaveArrowᵗ ∧ ¬Shootᵗ). With no action that supplies another arrow, it persists until shooting and remains absent afterward.

An agent needs a standard for deciding whether a conclusion is justified. Entailment, written KB ⊨ α, means that α is true in every model satisfying the KB. One compatible world where α is false defeats the entailment.

Keep exactly the compatible models

Model checking enumerates assignments, discards those that make any KB sentence false, and tests the query in those that remain. Suppose the KB contains A ∨ B and ¬A. Of the four assignments to A and B, only A false, B true satisfies both sentences. The KB entails B and ¬A. It fails to entail A because its surviving model makes A false.

In the wumpus KB, ¬P₁₁, B₁₁ ⇔ (P₁₂ ∨ P₂₁), B₂₁ ⇔ (P₁₁ ∨ P₂₂ ∨ P₃₁), ¬B₁₁ and B₂₁ use seven symbols. There are 128 assignments. Exactly three satisfy the KB: P₁₂ and P₂₁ are false, while P₂₂ and P₃₁ are respectively true/false, false/true or true/true. Thus ¬P₁₂ is entailed. P₂₂ varies across the three models, so neither P₂₂ nor ¬P₂₂ is entailed. These pit rules alone establish absence of a pit, not absence of the wumpus.

Distinguish the main logical tests

P ∨ ¬P is valid; P ∧ ¬P is unsatisfiable. P ⇒ Q and ¬P ∨ Q are equivalent. Equivalence requires entailment in both directions. A ∧ B entails A, but A allows models with B false, so the reverse entailment fails.

Turn a query into a contradiction test

KB ⊨ α exactly when KB ∧ ¬α is unsatisfiable. Adding the negated query looks for a world where the KB holds and the query fails. Finding none proves entailment; finding one gives a countermodel. Equivalently, α ⊨ β exactly when α ⇒ β is valid. Validity of α can itself be tested by checking whether ¬α is unsatisfiable.

The connective ⇒ belongs inside a sentence. The symbol ⊨ describes a relationship between sentences and their models. Similarly, "not entailed" can mean the query is ruled out or that it remains unknown. Check whether the negation is entailed before choosing between them.

Enumeration is sound and complete for propositional logic because it checks a finite set exhaustively. Depth-first enumeration takes O(2ⁿ) time and O(n) memory; 50 symbols already yield about 1.13 × 10¹⁵ assignments. Propositional entailment is co-NP-complete. Also check consistency: a KB with no models entails every sentence, because it has no compatible model that could violate any query.

A proof derives a query by applying rules to sentences already known. KB ⊢ α records a derivation; KB ⊨ α records a semantic guarantee across models. A sound proof procedure connects them: every conclusion it derives really follows. A complete procedure can derive every entailed conclusion within its intended language.

Apply rules to their premises

Modus Ponens takes P ⇒ Q and P to Q. And-Elimination takes P ∧ Q to either conjunct. If SensorOn ∧ Calibrated is known and SensorOn ⇒ ReadingAvailable is known, And-Elimination yields SensorOn, then Modus Ponens yields ReadingAvailable. Each line names the information and rule that justify it.

These rules preserve truth, but their restricted vocabulary makes them incomplete as a complete proof system. From P, the sentence P ∨ Q follows semantically, yet neither rule introduces ∨. A set of sound rules can still miss valid conclusions.

Rewrite without changing meaning

Useful equivalences can be applied in either direction:

• Double negation: ¬¬P ≡ P.
• Implication: P ⇒ Q ≡ ¬P ∨ Q.
• Contraposition: P ⇒ Q ≡ ¬Q ⇒ ¬P.
• Biconditional: P ⇔ Q ≡ (P ⇒ Q) ∧ (Q ⇒ P).
• De Morgan: ¬(P ∨ Q) ≡ ¬P ∧ ¬Q, and ¬(P ∧ Q) ≡ ¬P ∨ ¬Q.
• Distribution: P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R), with the dual law for ∧ over ∨.

Conjunction and disjunction also allow regrouping and reordering. These rewrites expose a sentence's useful structure without adding a new factual assumption.

For B₁₁ ⇔ (P₁₂ ∨ P₂₁) and ¬B₁₁, split the biconditional and select (P₁₂ ∨ P₂₁) ⇒ B₁₁. Contraposition gives ¬B₁₁ ⇒ ¬(P₁₂ ∨ P₂₁). Modus Ponens yields ¬(P₁₂ ∨ P₂₁); De Morgan yields ¬P₁₂ ∧ ¬P₂₁. And-Elimination then proves ¬P₁₂. The proof never needs to enumerate every cave layout.

Test an invalid shortcut

From P ⇒ Q and Q, inferring P is affirming the consequent. From P ⇒ Q and ¬P, inferring ¬Q is denying the antecedent. Both fail in the model P false, Q true. A server outage may stop a page loading, but a loading failure has other possible causes; absence of an outage does not ensure success either.

Proof finding is a search problem. The initial state contains the KB; an action applies an inference rule and adds its conclusion; the goal state contains the query. The proof length can serve as path cost. Selecting relevant sentences avoids spending effort on unrelated chains. Classical logic is monotonic: adding premises preserves earlier entailments. Default rules with exceptions need a different treatment because later information can withdraw an earlier default conclusion.

Resolution proves entailment by looking for a contradiction. Its input is conjunctive normal form (CNF): an AND of clauses, each an OR of literals. A one-literal clause is a unit clause. The empty clause has no possible true literal and represents falsehood.

Convert sentences to clauses

First eliminate ⇔ and ⇒. Next move negations inward with De Morgan's laws and double-negation elimination. Finally distribute ∨ over ∧. A biconditional can therefore create several clauses.

For B₁₁ ⇔ (P₁₂ ∨ P₂₁), the forward direction gives ¬B₁₁ ∨ P₁₂ ∨ P₂₁. The reverse gives ¬(P₁₂ ∨ P₂₁) ∨ B₁₁. Moving the negation inward and distributing yields ¬P₁₂ ∨ B₁₁ and ¬P₂₁ ∨ B₁₁. All three clauses are needed for the full biconditional.

Resolve one complementary pair

From P ∨ A and ¬P ∨ B, resolution derives A ∨ B. Whichever value P has, at least one remaining part must hold. Unit resolution uses a single-literal clause: P with ¬P ∨ B yields B. Duplicate literals are factored out, so resolving A ∨ B with A ∨ ¬B yields A.

Resolve exactly one complementary pair at a time. A ∨ B and ¬A ∨ ¬B are jointly satisfiable when A is true and B false. Removing both pairs would incorrectly yield the empty clause. Resolving on A alone produces B ∨ ¬B, a tautology that adds no constraint.

Refute the negated query

To prove KB ⊨ α, add ¬α, convert the combined sentence to CNF, and derive new resolvents. Reaching the empty clause proves that no countermodel exists.

For the pit query ¬P₁₂, add P₁₂. Resolve it with ¬P₁₂ ∨ B₁₁ to get B₁₁. Resolve that with the observed ¬B₁₁ to reach the empty clause. The proof establishes absence of the pit, not its presence: the positive pit literal was a temporary negated query.

A second example uses R ⇒ C, (C ∨ I) ⇒ G and R. The CNF clauses are ¬R ∨ C, ¬C ∨ G, ¬I ∨ G and R. Add ¬G. It resolves with ¬C ∨ G to give ¬C, which yields ¬R using the first clause. Resolving ¬R with R closes the refutation. No fact about I was required.

Propositional resolution is sound and refutation-complete. It terminates because finitely many symbols permit finitely many distinct clauses. If exhaustive closure produces no new clause and no contradiction, the query is not entailed. It need not derive every entailed sentence directly: from A alone, resolution does not construct A ∨ B.

Distribution can expand CNF exponentially. A Tseitin encoding introduces symbols for subformulas and yields linear-size CNF. The new sentence is equisatisfiable with the original; it need not be logically equivalent over the expanded vocabulary. Preserving satisfiability is enough for SAT-based contradiction tests.

Rules with one positive conclusion permit a simpler inference procedure than general resolution. A definite clause has exactly one positive literal; ¬A ∨ ¬B ∨ C is written A ∧ B ⇒ C. A fact has an empty body. A Horn clause has at most one positive literal, including a goal clause with none, such as A ∧ B ⇒ False.

Let facts drive the rules

Forward chaining starts with known facts. When every premise of a rule is known, add its head. Continue until the query appears or a fixed point adds nothing. Efficient implementations keep an agenda of new facts and a count of unmet premises per rule.

Take PowerOn, FanSpinning and LoadLow as facts. The rules are PowerOn ∧ FanSpinning ⇒ Cooling; Cooling ∧ LoadLow ⇒ TempNormal; PowerOn ⇒ LedLit; LedLit ∧ TempNormal ⇒ SystemOK; FanSpinning ⇒ NoiseHeard. Processing PowerOn enables LedLit and partly satisfies the cooling rule. FanSpinning enables Cooling and NoiseHeard. Cooling plus LoadLow gives TempNormal, then TempNormal plus LedLit gives SystemOK. NoiseHeard is a valid extra conclusion even though the query did not need it.

Let a query choose the rules

Backward chaining starts with SystemOK. Its rule requires LedLit and TempNormal. LedLit reduces to the known PowerOn. TempNormal requires Cooling and LoadLow; Cooling requires PowerOn and FanSpinning. Every leaf is a fact, so the query succeeds. The noise rule is never examined.

For definite-clause KBs and atomic queries, both methods are sound and complete with appropriate search control. Propositional forward chaining can run in time linear in KB size. At its fixed point, assigning true to derived symbols and false to all others gives a model of the definite clauses.

Handle cycles without losing answers

A ⇒ B and B ⇒ A give a naive backward procedure an endless loop. A branch can stop when its goal is already on the active goal stack. Successful subgoals can be cached, but a failure caused by a loop is temporary. With B ⇒ A, A ⇒ B, C ⇒ A and fact C, an early attempt to prove B while A is active can fail. After proving A from C, trying B again succeeds. Caching that first failure permanently would lose the proof. Tabling tracks dependent goals and revisits them when answers appear.

Chaining depends on the rule form. A ∨ B has two positive literals, so it is not Horn. Together with A ⇒ C and B ⇒ C, it entails C by considering both alternatives. No definite rule fires from the disjunction alone. General resolution can prove this conclusion even though simple chaining stalls.

A SAT solver searches for an assignment satisfying every clause in a CNF sentence. A returned model can be checked directly. An unsatisfiable result rules out all assignments. SAT is NP-complete, but structured instances often admit much faster solutions than exhaustive truth-table enumeration.

Reduce the search with DPLL

DPLL is depth-first backtracking with three shortcuts. A true literal satisfies its entire clause, while a fully false clause ends the branch. A pure symbol occurs with only one sign among unsatisfied clauses, so it can be set to satisfy those occurrences. A unit clause has only one remaining possible true literal, which must be set true. Repeating such forced choices is unit propagation.

Consider (A), (¬A ∨ B), (¬B ∨ C ∨ D), (¬C ∨ ¬D), (D ∨ E). E is pure, so set it true. The unit A forces A true, which forces B true. The remaining constraint C ∨ D and the clause ¬C ∨ ¬D require exactly one of C and D. Branch on C true; propagation forces D false. A, B, C and E true with D false satisfy every clause.

For (A ∨ B), (A ∨ ¬B), (¬A ∨ C), (¬A ∨ ¬C), branch on A. A false forces both B and ¬B; A true forces both C and ¬C. Both branches conflict, so the whole sentence is unsatisfiable.

Learn from conflicts

Conflict-driven clause learning (CDCL) extends this search. A learned clause blocks a combination responsible for a conflict. Backjumping skips irrelevant choices; variable activity guides branching; restarts change the search route; watched literals speed propagation. Learned clauses are justified by the formula, so they preserve its possible solutions.

Search by changing a complete assignment

WalkSAT begins with a random complete assignment. It chooses an unsatisfied clause and flips a variable in it, sometimes randomly and sometimes to leave the most clauses satisfied. Random moves help escape local traps. Starting with all five symbols false in the earlier example leaves (A) and (D ∨ E) false. Flipping A fixes (A) but breaks (¬A ∨ B). A move can repair one clause while damaging another.

For entailment, submit KB ∧ ¬α. Unsatisfiability proves α; a model is a counterexample. A WalkSAT timeout leaves both possibilities open. In large random 3-CNF formulas, the clause-to-variable ratio has an estimated transition near 4.26, with hard instances often near it. This is an ensemble pattern, not a cutoff that decides an individual formula. Clause structure and solver strategy also affect difficulty.

First-order logic describes objects and their relationships. Instead of giving every square an unrelated symbol, it can express a rule for all squares: ∀s (Breezy(s) ⇔ ∃r (Adjacent(r, s) ∧ Pit(r))). Quantifiers make generality part of the language.

Separate objects from claims

A constant names an object, such as Ada. A variable, such as x, ranges over objects. A function maps objects to an object: MotherOf(Ada) is a term referring to someone. A predicate forms a claim: Owns(Ada, Atlas) is true or false. A term may be a constant, variable or function applied to terms.

Book(x) is a sentence, not an object, so Owns(Ada, Book(x)) puts the wrong kind of expression in an argument position. Equality compares what terms refer to: MotherOf(Ada) = Clara says both terms denote the same object.

Evaluate a sentence in a model

A first-order model supplies a nonempty domain and an interpretation. Constants denote domain objects, predicates denote relations, and functions give outputs for every suitable tuple of domain objects. A universally quantified sentence must hold for every possible value of its variable; an existential sentence needs at least one witness.

Let the domain be {a, b, k}; Ada names a, Ben names b and Atlas names k. Person contains a and b, Book contains k, and Owns contains only (a, k). Owns(Ada, Atlas) is true. ∃x (Book(x) ∧ Owns(Ben, x)) is false because Ben owns no object. ∀x (Person(x) ⇒ ∃y (Book(y) ∧ Owns(x, y))) is false because Ben is a counterexample. Yet every book has an owner: ∀x (Book(x) ⇒ ∃y Owns(y, x)) holds.

Make modeling assumptions explicit

Standard FOL does not impose these database assumptions. Book(Atlas), Book(Beowulf), Owns(Ada, Atlas) and Owns(Ada, Beowulf) leave open whether the two names denote the same book and whether Ada owns more books. Under database semantics, they describe exactly two owned books.

To obtain that exact claim in standard semantics, keep the four facts and add ¬(Atlas = Beowulf) and ∀x ((Book(x) ∧ Owns(Ada, x)) ⇒ (x = Atlas ∨ x = Beowulf)). The inequality establishes two distinct books; the universal restriction excludes additional owned books.

First-order models can have arbitrarily large domains, so the finite enumeration method for propositional models does not provide a general decision procedure here. Proof methods work with the sentences' structure instead. A free variable needs an assignment for evaluation; bind variables when writing a closed claim for the KB.

Translation begins by deciding what the sentence claims about each object. Quantifier scope, implication direction and equality determine the meaning; predicate names alone do not fix it. Parentheses make the intended scope visible.

Use the right connective with a quantifier

"Every cat is a mammal" becomes ∀x (Cat(x) ⇒ Mammal(x)). An object outside the category passes the implication without being a cat. Writing ∀x (Cat(x) ∧ Mammal(x)) incorrectly makes everything a cat.

"Some cat is black" becomes ∃x (Cat(x) ∧ Black(x)). The witness must satisfy both properties. With ∃x (Cat(x) ⇒ Black(x)), any non-cat is already a witness, even in a world with no black cats. Universal category rules usually use implication; existential category claims usually use conjunction.

Check who can depend on whom

∀x ∃y Loves(x, y) permits a different loved person for each x. ∃y ∀x Loves(x, y) requires one person loved by everyone. In a two-person world where each loves only the other, the first holds and the second fails. Swapping quantifiers of different kinds can change a claim; swapping two adjacent universal quantifiers or two adjacent existential quantifiers preserves it.

Negation swaps quantifiers: ¬∀x P(x) ≡ ∃x ¬P(x), and ¬∃x P(x) ≡ ∀x ¬P(x). Therefore "Not every student passed" means ∃x (Student(x) ∧ ¬Passed(x)). It requires a student who failed; it does not claim that every student failed.

Express direction and number

"Only members borrow" means ∀x (Borrows(x) ⇒ Member(x)). Borrowing is enough to establish membership, while membership alone says nothing about borrowing. "No reptile is a mammal" means ∀x (Reptile(x) ⇒ ¬Mammal(x)).

To express at least two owned books, write ∃x ∃y (Book(x) ∧ Book(y) ∧ Owns(Ada, x) ∧ Owns(Ada, y) ∧ ¬(x = y)). The inequality matters: two variable names may refer to the same object. Exactly one uses a witness plus uniqueness: ∃x (Book(x) ∧ Owns(Ada, x) ∧ ∀y ((Book(y) ∧ Owns(Ada, y)) ⇒ y = x)).

Give definitions both directions

A sibling definition can be ∀x ∀y (Sibling(x, y) ⇔ (¬(x = y) ∧ ∃p (Parent(p, x) ∧ Parent(p, y)))). The forward direction constrains siblings; the reverse lets shared-parent facts establish siblinghood. A one-way implication supplies only half that meaning.

In an agent domain, diagnostic rules run from observations to possible causes, while causal rules run from causes to effects. "Every breezy square has an adjacent pit" is diagnostic. "Every pit makes every adjacent square breezy" is causal. Together they support the full breeze biconditional. Finish a translation by checking every variable's binding and testing a small world where the English claim should fail.

Building a useful knowledge base is a modeling task. Formal notation only helps after the relevant questions, objects and relationships have been chosen. Knowledge engineering turns those choices into axioms that can be checked against intended examples.

Build around the questions

A practical sequence is to identify the task, gather relevant knowledge, choose a vocabulary, write general axioms, add instance facts, ask queries, and debug the results. Start with concrete questions such as "Can this student enroll in this course?" That question determines what the representation must support.

For enrollment, use Student(s), Course(c), Prereq(p, c), Passed(s, c) and CanEnroll(s, c). Prereq(p, c) means that p must be passed before c; reversing its arguments would reverse the dependency. A rule is ∀s ∀c ((Student(s) ∧ Course(c) ∧ ∀p (Prereq(p, c) ⇒ Passed(s, p))) ⇒ CanEnroll(s, c)). It requires every prerequisite, not merely one.

Separate reusable rules from an instance

Suppose the facts are Student(Mia), Course(AI), Prereq(Logic, AI), Prereq(Programming, AI), Passed(Mia, Logic) and Passed(Mia, Programming). The general rule can be reused for other students and courses, while these instance facts describe one case.

Under standard FOL, these facts leave open additional prerequisites for AI. A compatible model could include an unpassed third prerequisite, so CanEnroll(Mia, AI) is not yet entailed. Add ∀p (Prereq(p, AI) ⇔ (p = Logic ∨ p = Programming)) to complete the list. Now every prerequisite is one of the two passed courses, and the enrollment rule applies. A closed-world database can obtain the same answer by treating absent prerequisite facts as false.

Choose what becomes an object

An ontology is the vocabulary and its structural assumptions. Red(x) treats red as a property. Color(x, Red) makes Red an object, allowing ∃c (Color(x, c) ∧ Color(y, c)) to express a shared color. This move is reification: it lets the language talk about a property or category as something in its own right.

ASK can request whether CanEnroll(Mia, AI) follows. ASKVARS can request bindings for CanEnroll(x, AI), returning a substitution such as {x/Mia}. The same KB supports both truth questions and queries for matching objects.

Debug meaning, not just syntax

A missing axiom can block a desired entailment; an incorrect axiom can support an unwanted one. Test positive examples, negative examples and boundary cases. The rule ∀c (Course(c) ⇒ ∃t Teaches(t, c)) is too strong if some courses have no teacher yet. The rule ∀p ∀c (Prereq(p, c) ⇒ Passed(Mia, p)) is too strong because it grants Mia every prerequisite of every course.

Predicate names are labels for the reasoner. Calling a relation Prereq supplies no enrollment policy by itself. The rules must connect prerequisite facts, passed courses and eligibility in the intended direction.

First-order inference works with patterns containing variables. Substitution replaces variables with terms; unification finds replacements that make two expressions identical. Together they let one general rule serve many particular facts without generating every possible instance first.

Instantiate quantified sentences carefully

Universal Instantiation replaces a universally bound variable with any ground term. From ∀x (Cat(x) ⇒ Mammal(x)), derive Cat(Tom) ⇒ Mammal(Tom), or the corresponding instance with MotherOf(Tom). A ground term contains no variable.

Existential Instantiation introduces a fresh witness name. From ∃x (Crown(x) ∧ OnHead(x, John)), introduce a new constant C₁ and add Crown(C₁) and OnHead(C₁, John). Naming Ben as the witness instead would wrongly identify an unspecified object with an existing one. The expanded KB preserves satisfiability, not equivalence in the enlarged vocabulary.

Propositionalization generates ground instances, then uses propositional reasoning. Function symbols can produce infinitely many terms: Ada, MotherOf(Ada), MotherOf(MotherOf(Ada)), and so on. Entailed first-order queries have finite proofs, but a general prover may run forever when the query is not entailed. This is semidecidability.

Find a consistent substitution

To unify Knows(Ana, x) with Knows(y, Bo), first match the predicate and arity. The first arguments require y = Ana; the second require x = Bo. The substitution {y/Ana, x/Bo} makes both expressions Knows(Ana, Bo).

Knows(Ana, x) and Knows(y, MotherOf(y)) instead give {y/Ana, x/MotherOf(Ana)}. A binding must be propagated through the other terms. If the same variable x occurs in both expressions Knows(Ana, x) and Knows(x, Bo), it would need to become both Ana and Bo, so syntactic unification fails.

Variables in separately quantified sentences are independent. Standardizing apart renames them before combining sentences. Renaming the second x to z in that last pair allows {z/Ana, x/Bo}. This preserves the intended independence of two rules' local variables.

A most general unifier (MGU) imposes no unnecessary bindings. Knows(Ana, x) and Knows(y, z) unify with {y/Ana, x/z}; also setting z to Ana would specialize the result without need. The occurs check rejects x = MotherOf(x), since a finite term cannot contain itself. Prolog's ordinary unification may allow cyclic terms, so its behavior needs care when finite-term FOL is intended.

Apply the matched rule

Generalized Modus Ponens matches every premise under one consistent substitution. Owns(Ada, Atlas) and Book(Atlas) match Owns(x, y) ∧ Book(y) ⇒ Reader(x) with {x/Ada, y/Atlas}, yielding Reader(Ada). Matching one premise with y = Atlas and another with y = Beowulf would not justify firing the rule: shared variables enforce shared objects.

A first-order definite clause has atomic premises and one atomic conclusion, with its variables universally understood. Forward and backward chaining use unification to apply these rules to named objects. Datalog keeps this rule form and excludes function symbols, giving a finite space of possible ground facts in the usual finite-database setting.

Derive reachable locations

Take Link(A, B), Link(B, C) and Link(C, D). Use Link(x, y) ⇒ Reach(x, y), and Link(x, y) ∧ Reach(y, z) ⇒ Reach(x, z). In synchronous rounds, each rule reads the facts available before that round.

Round 1 derives Reach(A, B), Reach(B, C) and Reach(C, D). Round 2 adds Reach(A, C) and Reach(B, D). Round 3 adds Reach(A, D). Round 4 adds nothing. There are six Reach facts at the fixed point. An implementation that immediately reuses new facts may find them in a different order but reaches the same closure.

With n constants and predicates of arity at most k, only finitely many tuples are possible; an upper bound is p · nᵏ for p predicates. In contrast, NatNum(0) and NatNum(n) ⇒ NatNum(S(n)) generate endlessly deeper terms. Function symbols remove the finite-domain guarantee.

Matching a multi-premise rule is a constraint problem. A selective premise can greatly reduce the substitutions considered next. Incremental forward chaining focuses on rules affected by newly added facts. Rete networks retain partial matches across updates, avoiding repeated work in production-rule systems.

Work backward with bindings

To prove Reach(A, D), try the direct-link rule, which requires the absent Link(A, D). The recursive rule instead requires Link(A, y) and Reach(y, D). The first binds y to B. Continuing through B and C reaches the known Link(C, D). The query Reach(A, w) has three answers: w = B, C or D.

Prolog writes rules with the head first and uses uppercase variables and lowercase constants:

reach(X, Y) :- link(X, Y).
reach(X, Z) :- link(X, Y), reach(Y, Z).

It tries clauses top to bottom and premises left to right using depth-first backward chaining. Arithmetic can use N is M + 1. Negation as failure, written \+ p, succeeds if the attempt to prove p finitely fails. It is an operational test of failure, not a general proof of classical negation.

Keep recursion from trapping the search

Putting reach(X, Y) first in the recursive body can immediately call the same unresolved goal again. Base clauses first and recursion that consumes a link help, but cycles can still trap unsuccessful searches. Tabling records subgoal answers and manages repeated dependencies. Forward chaining is complete for finite Datalog; naive depth-first backward search needs this kind of control to avoid missing reachable answers behind infinite branches.

First-order resolution extends clause reasoning with unification. It can prove conclusions involving unnamed objects because Skolem terms preserve the dependencies of existential witnesses. As in propositional refutation, begin with the KB and the negation of the query.

Prepare first-order clauses

Eliminate ⇔ and ⇒, move negations inward, standardize bound variables, Skolemize existentials, drop universal quantifiers, then distribute ∨ over ∧. Moving negation first matters because ¬∀x P(x) becomes ∃x ¬P(x), changing the kind of witness required.

For "Every course has a teacher," ∀c (Course(c) ⇒ ∃t Teaches(t, c)), the existential teacher can depend on c. Introduce a fresh function T(c) to obtain ¬Course(c) ∨ Teaches(T(c), c). A single constant would impose one shared teacher, which the original sentence never requires. For ∃t ∀c (Course(c) ⇒ Teaches(t, c)), a fresh constant is appropriate because the witness precedes the universal quantifier.

"Not every bird flies" becomes ∃x (Bird(x) ∧ ¬Flies(x)), then Bird(B₁) and ¬Flies(B₁). Both clauses use the same fresh witness. Skolemization preserves satisfiability; it is not ordinary equivalence over the extended vocabulary.

Apply a unifier to the whole resolvent

Standardize the two clauses apart. Find complementary literals that unify, remove them and apply their MGU to every remaining literal. Factoring also merges unifiable literals within a clause. Resolution with factoring is refutation-complete for first-order clauses.

Take ¬Course(c) ∨ Teaches(T(c), c), ¬Teaches(u, v) ∨ Staff(u), and Course(Logic). The query is ∃w Staff(w); its negation gives ¬Staff(w), universally quantified. Resolve the course fact with the first clause to obtain Teaches(T(Logic), Logic). Resolve with the second under {u/T(Logic), v/Logic}, giving Staff(T(Logic)). Resolve with ¬Staff(w) under {w/T(Logic)} to reach the empty clause. A staff member exists even though the KB never gives that person an ordinary name.

Control the clause search

Unit preference chooses short clauses first. Set of support requires a parent from the negated query or its descendants and preserves completeness when the remaining KB is satisfiable. Input resolution requires an original parent at every step and is complete for Horn KBs. Subsumption removes a weaker clause already covered by a stronger general one, such as deleting P(Ana) ∨ Q(Bo) when P(x) is known.

Equality needs dedicated treatment: equality axioms, rewriting by equations through demodulation, or inferences such as paramodulation. Pure syntactic resolution alone does not capture every meaning of equality. A fair complete search finds a contradiction for every unsatisfiable first-order clause set, but can run forever otherwise. Resolution-based provers include Vampire and E; EQP proved the Robbins conjecture in 1996.

An ontology organizes a domain's categories, objects, relations and assumptions. An upper ontology supplies broad ideas such as objects, events and time; a domain ontology supplies the distinctions useful in a particular field. Clinical and biological ontologies illustrate why a useful shared vocabulary often serves a specific community.

Keep membership and subclass separate

A category can appear as a predicate, Laptop(x), or as an object, Laptops. Membership x ∈ Laptops says an individual belongs to it. Laptops ⊂ Computers says every laptop is a computer. A taxonomy arranges such subclass relationships in a hierarchy. If every computer has a processor, laptops inherit that property.

Subclass is transitive: Penguins ⊂ Birds and Birds ⊂ Animals give Penguins ⊂ Animals. Membership is not transitive. Pingu ∈ Penguins and Penguins ∈ Species do not make Pingu a species. One statement concerns an individual bird; the other concerns a category treated as an object.

Categories are disjoint when they share no members. An exhaustive decomposition covers every member of the parent. A partition does both: negative integers, zero and positive integers partition the integers. Exhaustiveness permits overlap unless disjointness is also stated.

Represent parts, events and inherited values

PartOf describes composition, not category membership. PartOf is transitive: a spoke belonging to a wheel that belongs to a bicycle is part of the bicycle. A bicycle is not thereby a kind of wheel. Events can be objects too: Happens(e, t), Initiates(e, f, t) and HoldsAt(f, t) connect events to changing fluents. Switching on a lamp initiates a fluent that persists until an event terminates it.

A semantic network draws objects and categories as nodes with labeled relations. In a network with defaults, "birds normally fly" can supply a value inherited by ordinary birds, while a more specific penguin category overrides it. This is different from asserting the exceptionless classical axiom ∀x (Bird(x) ⇒ Flies(x)), which would also apply to penguins.

Choose the reasoning language

Description logics support subsumption, classification and consistency checks. A definition can classify a person with at least three children into an appropriate category. These logics form the basis of OWL's description-logic languages.

Default reasoning is nonmonotonic: learning a bird is a penguin can retract a flying default. Circumscription minimizes abnormal cases in rules such as Bird(x) ∧ ¬Abnormal(x) ⇒ Flies(x). Default logic permits conclusions while they remain consistent with the knowledge. Truth maintenance systems record support so that conclusions depending on a withdrawn belief can be removed.

A knowledge graph stores entities and their relationships as a directed graph. A simple edge becomes a triple: subject, predicate, object. For example, (Ada, worksAt, Lab) corresponds to WorksAt(Ada, Lab); (Ada, type, Researcher) states category membership. A schema gives these labels shared meaning and enables further inference.

Distinguish the web standards

RDF represents graphs as triples. Subjects are IRIs or blank nodes, predicates are IRIs, and objects may also be literal values. IRIs identify resources across datasets; a blank node represents a resource without giving it a global identifier. RDFS adds classes, subclass relations, and property domain and range. OWL provides richer ontology definitions. SPARQL matches graph patterns to return variable bindings. Property graphs offer another model with key–value properties on nodes and edges; Cypher and GQL are query languages for that family.

If Ada is typed Researcher and Researcher is a subclass of Scientist, a subclass rule derives that Ada is a Scientist. This is first-order forward chaining over Member(x, c) ∧ Subset(c, d) ⇒ Member(x, d). A graph query engine needs the relevant entailment support or materialized conclusions to expose this inferred fact.

Match a query and preserve detail

With ex: declared as an IRI prefix, a query can be:

SELECT ?p WHERE {
  ?p a ex:Researcher .
  ?p ex:worksAt ex:Lab .
}

The same ?p must satisfy both patterns. It is a join, not two unrelated searches. Results are bindings such as ?p = ex:Ada, like substitutions in logical queries.

A binary edge cannot by itself express every role in a dated event. For an award, create an event or statement node and connect it to the recipient, prize and year. This keeps one award's details together and avoids accidentally attaching the date to every award of that type. Wikidata supports statement qualifiers for such detail.

Separate absent, inferred and predicted links

RDF and OWL use an open-world reading: a missing spouse edge leaves the relationship unknown. Closed-world applications make a different choice about missing facts. A query's empty result reports lack of a match under that query setup; it does not by itself establish a universal negative fact.

Wikidata, DBpedia, Google's Knowledge Graph and internal organizational graphs support factual queries, record linking, recommendations and retrieval for generative systems. Their facts can be incomplete or outdated. Entity resolution identifies records referring to the same thing even when identifiers differ.

Embeddings assign vectors to entities and relations. In TransE, the head vector plus the relation vector is trained to be close to the tail vector. A high score suggests a missing link; it is a statistical prediction. Logical inference derives a consequence from stated facts and rules. Keep this difference visible when deciding whether a new edge belongs among verified facts.

Classical planning seeks actions that take a known initial state to a goal. The model is fully observable, deterministic, discrete and single-agent; the world changes through the modeled actions. A factored representation describes each state through fluents, so a planner can reason about what each action changes.

Write the state and action schemas

In the basic STRIPS-style fragment of PDDL, a state lists true ground atomic fluents. Unlisted fluents are false under the closed-world assumption. The reusable domain declares predicates and action schemas; the problem declares objects, the initial state and a goal. PDDL was introduced for the 1998 planning competition, building on STRIPS.

An action schema has parameters, a precondition and effects. Go(r, from, to) requires At(r, from) and Connected(from, to); it adds At(r, to) and deletes At(r, from). Pick(r, p, l) requires At(r, l), In(p, l) and HandEmpty(r); it adds Holding(r, p) and deletes In(p, l) and HandEmpty(r). Drop requires location and holding; it adds the package's location and an empty hand, and deletes holding.

A ground action applies only when its preconditions hold. Its update is RESULT(s, a) = (s − DEL(a)) ∪ ADD(a). Other fluents persist, including static Connected facts. This implicit persistence handles the frame problem without a separate axiom for every unaffected fluent.

Follow a four-action delivery

Initially R is at Dock, Box is at Shelf and R's hand is empty. Connected links join Dock to Shelf and Shelf to Packing in both directions. The goal is In(Box, Packing).

1. Go(R, Dock, Shelf) changes R's location and preserves the box and hand facts.
2. Pick(R, Box, Shelf) removes the box from the shelf and makes R hold it.
3. Go(R, Shelf, Packing) moves R while preserving Holding(R, Box).
4. Drop(R, Box, Packing) places the box at Packing and frees the hand.

The goal leaves the robot's final location unspecified except where the actions require it. Goals generally describe many acceptable states, not one complete state.

Read and check a schema

(:action pick
 :parameters (?r ?p ?l)
 :precondition (and (at ?r ?l) (in ?p ?l) (hand-empty ?r))
 :effect (and (holding ?r ?p)
              (not (in ?p ?l)) (not (hand-empty ?r))))

Omitting a delete effect can leave a robot in two places or a package both held and on a shelf. Putting a required condition only in an effect makes the action create it instead of checking it.

In blocks world, moving a clear block b from x onto a clear block y requires On(b, x), Clear(b), Clear(y), Block(b), Block(y) and ¬(b = y). It adds On(b, y) and Clear(x), and deletes On(b, x) and Clear(y). The distinctness and block checks prevent self-stacking and treating the table like a single block. A separate MoveToTable action keeps the table available for other blocks.

A planning model defines a search space, but choosing useful actions is still difficult. Progression searches forward through complete states. Regression searches backward through the conditions that a preceding state must satisfy. Both can reuse general search methods while exploiting action structure.

Search from either end

Progression starts at the initial state and applies applicable ground actions. It can waste effort on irrelevant actions: one robot, 20 boxes and 10 locations already give 200 possible ground Pick combinations before applicability filtering.

Regression considers an action that achieves a goal literal without negating another goal literal. Regress a goal set g through a by removing achieved literals and adding preconditions: g′ = (g − EFFECT(a)) ∪ PRECOND(a). EFFECT includes signed positive and negative literals. Reject an inconsistent result containing a literal and its negation.

For In(Box, Packing) ∧ At(R, Dock), regressing through Drop(R, Box, Packing) gives Holding(R, Box) ∧ At(R, Packing) ∧ At(R, Dock). These conditions conflict with the intended single-location invariant. A valid plan must deliver the box before the robot's final return. Regressing through Go(R, Shelf, Dock) instead gives In(Box, Packing) ∧ At(R, Shelf) ∧ Connected(Shelf, Dock), which preserves the delivered package.

Estimate distance using simpler problems

A heuristic is admissible when it never overestimates the remaining optimal cost. A* with an admissible heuristic finds an optimal plan. Counting unsatisfied goals is not always admissible: a single action might achieve several.

Ignoring preconditions makes all actions immediately usable. Ignoring delete effects makes progress permanent, for problems expressed with positive preconditions and goals. Negative conditions must first be compiled into explicitly maintained positive fluents. The optimal relaxed-plan length h⁺ is a lower bound on real plan length, but computing it is NP-hard. FF finds a relaxed plan quickly without guaranteeing its optimality; its length can overestimate h⁺ and is not guaranteed admissible.

For the warehouse delivery plus return goal, the real shortest plan has six actions: go to Shelf, pick, go to Packing, drop, return to Shelf, return to Dock. Delete relaxation needs only the first four because At(R, Dock) remains true after departure. Thus h⁺ = 4 while the real cost is 6. The unsatisfied-goal count starts at only 1 and misses most of that work.

Combine estimates without double counting

A planning graph alternates possible fluent and action levels, with mutex links marking incompatible pairs. A goal's first appearance gives a level estimate. Taking the maximum of individual goal levels is admissible; adding them can count shared work repeatedly. State abstraction removes some fluents to reduce the state space. Subgoal decomposition also benefits from checking shared actions: the maximum of admissible subgoal costs is safe, while their sum needs extra justification.

Planning methods differ in what they search over: states, truth assignments, ordering constraints or refinements of expert procedures. Their usefulness depends on subgoal interaction and the assumptions the model makes about execution.

Recognize interacting subgoals

In the Sussman anomaly, C is on A, with A and B on the table. The goal is On(A, B) ∧ On(B, C). Completing the A-on-B subgoal first blocks the later placement of B. Placing B onto C immediately leaves A buried. A shortest plan frees A first, then builds the stack from the bottom: move C to the table, move B onto C, then move A onto B. The three moves interleave preparation and goal achievement.

Encode a bounded plan as SAT

SATPlan chooses a horizon T. It asserts initial fluents at time 0, goal fluents at T, action preconditions, successor-state constraints and exclusions for incompatible actions. A satisfying assignment selects actions forming a plan. An unsatisfiable result excludes plans within that encoding and horizon.

Trying horizons in order finds the smallest satisfiable horizon. With parallel actions this minimizes layers, not necessarily the total number of actions. A stopping bound is needed to turn repeated unsatisfiable horizons into a conclusion that no plan exists.

Keep only the necessary order

Partial-order planning records actions, order constraints and causal links. A link A —p→ B says A establishes precondition p for B. An action C that could delete p between them is a threat. Demotion orders C before A; promotion orders it after B. Unrelated actions can remain unordered until execution, following least commitment.

HTN planning refines high-level tasks through a library of methods. DeliverBox can become travel to the box, pick it up, travel to the destination and drop it. These methods encode expert procedures, so the search can focus on useful refinements instead of considering every primitive action at every point.

Match the model to the world

Plan existence for general propositional STRIPS is PSPACE-complete. Blocks world has an easier existence problem for possible arrangements: clear the blocks to the table and rebuild, using at most 2n moves for n blocks. Finding a shortest blocks-world plan is still NP-hard.

Classical models leave out uncertain outcomes, hidden state and action durations. Conformant plans work without observations, contingent plans branch on observations, online replanning responds to execution differences, and scheduling handles times and resources. A missing battery precondition can make a model-valid plan fail physically. Execution monitoring checks this gap. Automated planning has reached real systems, including NASA's Remote Agent on Deep Space 1 in 1999.