Chapter 7 – Logical Agents (Vocabulary Flashcards)

Vocabulary flashcards covering the key terms and definitions from Chapter 7 – Logical Agents, including knowledge-based reasoning, propositional logic, inference techniques, and SAT solving.

Knowledge-based agent

An intelligent system that selects actions by reasoning over an internal knowledge base rather than by fixed rules or reflexes.

Knowledge base (KB)

A collection of sentences expressed in a formal language that represents what an agent knows about the world.

TELL operation

The procedure for adding new sentences (axioms or percepts) to a knowledge base.

ASK operation

The procedure for querying a knowledge base to determine whether a sentence is entailed.

Inference engine

The algorithmic component of a knowledge-based agent that derives new sentences from the KB.

Knowledge level

A description of an agent in terms of what it knows rather than how that knowledge is implemented.

Wumpus World

A grid-based test environment containing a Wumpus, pits, breezes, stenches, and gold, used to illustrate knowledge-based reasoning.

Entailment (⊨)

The property that a sentence α is true in every model in which a knowledge base KB is true; written KB ⊨ α.

Model

A formally structured world (assignment of truth values to proposition symbols) against which sentence truth is evaluated.

Model checking

Proving KB ⊨ α by enumerating all models of KB and verifying that α holds in each.

Soundness

An inference procedure is sound if every sentence it derives from KB is actually entailed by KB.

Completeness

An inference procedure is complete if it can derive every sentence that is entailed by the knowledge base.

Propositional (Boolean) logic

A formal language whose atomic elements are proposition symbols connected by logical connectives such as ¬, ∧, ∨, ⇒, ⇔.

Syntax (of logic)

The set of rules that defines which symbol combinations form well-formed sentences.

Semantics (of logic)

The rules that assign meanings (truth conditions) to well-formed sentences.

Truth table

A table that lists the truth value of a logical connective or sentence for every possible assignment of its symbols.

Validity (tautology)

A sentence that is true in all possible models (e.g., A ∨ ¬A).

Satisfiability

The property of a sentence being true in at least one model.

Contradiction (unsatisfiable)

A sentence that is false in all models (e.g., A ∧ ¬A).

Deduction theorem

States that KB ⊨ α iff the implication (KB ⇒ α) is valid.

Logical equivalence (≡)

Two sentences are logically equivalent if each entails the other; they are true in exactly the same models.

Conjunctive Normal Form (CNF)

A conjunction of disjunctions of literals; every propositional sentence can be converted to an equivalent CNF.

Resolution rule

A single sound and complete inference rule for CNF: from (A ∨ X) and (¬A ∨ Y) derive (X ∨ Y).

Proof by contradiction (refutation)

Technique that shows KB ⊨ α by proving KB ∧ ¬α is unsatisfiable.

Horn clause

A disjunction of literals containing at most one positive literal; can be written as an implication (A ∧ B ⇒ C).

Forward chaining

A data-driven inference method that repeatedly applies Modus Ponens to derive new facts until the query is reached.

Backward chaining

A goal-driven inference method that works backward from the query, proving subgoals until known facts are reached.

Modus Ponens

Valid inference rule: from (α ⇒ β) and α, conclude β.

Unit resolution

Special case of resolution where one premise is a single literal; often used in forward chaining.

Pure symbol

A proposition symbol that appears with only one polarity (always positive or always negated) in all clauses; useful in DPLL.

Unit clause

A clause with exactly one unassigned literal, forcing that literal’s value during DPLL search.

SAT problem

The task of determining whether a propositional sentence is satisfiable (has at least one model).

DPLL algorithm

The Davis–Putnam–Logemann–Loveland backtracking algorithm for deciding SAT using pure-symbol and unit-clause heuristics.

Component analysis

DPLL optimization that splits a clause set into independent subproblems for faster solving.

Degree heuristic

Variable-ordering strategy that selects the symbol appearing in the most remaining clauses.

Intelligent backtracking

DPLL enhancement that backtracks directly to the decision responsible for a conflict, skipping irrelevant levels.

Random restart

SAT-solving technique that abandons a search path after little progress and starts with a fresh random ordering.

Effective Propositional Model Checking

A family of SAT-based algorithms that perform general propositional inference more efficiently than exhaustive enumeration.

Inference

The process of deriving new sentences from existing ones using sound rules of logic.

Implementation level

The lower level that describes how an agent’s knowledge and reasoning are actually represented in hardware or software.

Stench (Wumpus percept)

Sensor signal indicating the agent is in a square adjacent to the Wumpus.

Breeze (Wumpus percept)

Sensor signal indicating the agent is in a square adjacent to a pit.