To overcome the limitations of search-based agents, we introduce knowledge-based agents with three core components:

• Knowledge base (KB): Central repository where the agent stores its understanding of the world — its memory and model of reality, used to make decisions.
• Sentences: The KB contains sentences — formal statements about the world in a knowledge representation language with defined syntax and semantics.
• TELL and ASK operations: Two fundamental ways the agent interacts with its KB:
  • TELL — update the KB with new knowledge.
  • ASK — query the KB for guidance on what action to take.

A knowledge base can contain two types of sentences:

• Axioms — sentences taken as given, without being derived from other sentences.
• Inferences — sentences derived from existing sentences using rules of reasoning.

Propositional logic (also called zero-order logic) is the simplest form of logic for knowledge representation.

• Objects — sentences or formulae that encode information and denote statements about the world.
• Atoms — basic sentences; the building blocks of propositional logic, denoted P, Q, R, S, …
• Logical connectives — connect atoms to form compound formulae (e.g., if-then, and, or).
• Inference — derive new information from existing knowledge using syntactic rules.

1. True ✓
2. True (∧ S2) ✗ — (∧ AP) is not a valid connective
3. S1 →→ S2 ✗ — →→ is not a valid connective
4. ¬¬S1 ✓
5. S1 → ¬S2 ✓
6. S1 ¬→ S2 ✗ — ¬→ is not a valid connective

• Entailment (α ⊨ β) — the truth of one sentence requires the truth of another. In every model where α is true, β must also be true.
• Satisfaction — sentence α is true in model m. We write M(α) for the set of all models of α.
• Model checking — determine whether KB ⊨ α, i.e. M(KB) ⊆ M(α): in every model where KB is true, α must also be true.

To check whether KB ⊨ α:

1. Identify all propositional symbols appearing in KB and α.
2. Construct a complete truth table listing all 2ⁿ possible truth value combinations for n symbols.
3. Evaluate both KB and α in each row.
4. Select the models where KB is true — this is M(KB).
5. Check whether α is also true in all those models:
   • If yes: KB ⊨ α (entailment holds).
   • If no: KB ⊭ α (entailment does not hold).

What the KB encodes:

• Nothing in [1,1] → no adjacent pit or wumpus
• Breeze in [2,1] → P₂,₂ ∨ P₃,₁
• Stench in [1,2] → W₁,₃ ∨ W₂,₂

A world is KB-consistent iff both conditions hold: Breeze in [2,1] and Stench in [1,2].

Newly eliminated — all 8 worlds in the W₂,₂ group:

8 surviving worlds — pit constraints still to be applied:

Newly eliminated from the 8 remaining W₁,₃ worlds (no P₂,₂ and no P₃,₁):

Newly eliminated from the 6 remaining worlds:

Theorem proving applies inference rules directly to sentences in the KB to construct a proof — without enumerating models.

• Logical equivalence (≡): α ≡ β iff α and β are true in the same set of models. Standard equivalences apply (e.g., commutativity of ∧).
• Validity: A sentence is valid if it is true in all models (e.g., P ∨ ¬P).
• Deduction theorem: α ⊨ β iff the sentence (α → β) is valid.
• Satisfiability: A sentence is satisfiable if it is true in at least one model.

Sound inference rules derive new sentences without enumerating models:

• Modus Ponens (α → β, α | β): If α → β and α are both given, then β can be inferred.
• And-Elimination (α ∧ β | β): From a conjunction, any conjunct can be inferred individually.
• Biconditional elimination: α ↔ β ≡ (α → β) ∧ (β → α)
• Contraposition: (α → β) ≡ (¬β → ¬α)
• De Morgan: ¬(α ∧ β) ≡ (¬α ∨ ¬β)  and  ¬(α ∨ β) ≡ (¬α ∧ ¬β)
• All logical equivalences can be used as inference rules in either direction.

KB:

• R1: S_A ↔ A_A
• R2: S_B ↔ A_B
• R3: ¬A_A
• R4: ¬A_B

1. Biconditional elimination on R1: S_A ↔ A_A ≡ (S_A → A_A) ∧ (A_A → S_A) → R5
2. And-Elimination on R5: extract A_A → S_A → R6
3. Contraposition on R6: A_A → S_A ≡ ¬A_A → ¬S_A → R7
4. Modus Ponens with R7 and R3 (¬A_A): derive ¬S_A → R8
5. Apply same steps for room B → derive ¬S_B → R9: ¬S_A ∧ ¬S_B
6. De Morgan: ¬S_A ∧ ¬S_B ≡ ¬(S_A ∨ S_B)

• Knowledge base (KB)
• Sentence
• Axiom
• Inference
• TELL operation
• ASK operation

1. A doctor observes a patient has a fever and concludes they likely have an infection.
2. Every time a server is overloaded, response time increases. A developer concludes high load causes slow responses.
3. A fire alarm is sounding. The safety officer concludes there is probably smoke somewhere.
4. If the database is locked, queries will fail. The database is locked — therefore queries will fail.
5. Overloading a CPU causes it to throttle. The CPU is overloaded — therefore it will throttle.

1. True
2. True ∧ S2
3. S1 →→ S2
4. ¬¬S1
5. S1 → ¬S2
6. S1 ¬→ S2

1. A → (B ∨ ¬A)
2. (A ↔ B) ∧ ¬B
3. ¬(A ∧ B) ↔ (¬A ∨ ¬B)

1. KB = {P → Q, P},   α = Q.   Does KB ⊨ α?
2. KB = {P ∨ Q, ¬P},   α = Q.   Does KB ⊨ α?
3. KB = {P ↔ Q},   α = P ∧ Q.   Does KB ⊨ α?

• R1: S_A ↔ A_A   (smoke in A iff alarm in A sounds)
• R2: S_B ↔ A_B   (smoke in B iff alarm in B sounds)
• R3: A_A   (alarm in A is sounding)
• R4: ¬A_B   (alarm in B is not sounding)