Logical Agents

Knowledge-Based Agents

Agents that maintain an internal Knowledge Base (KB).

• KB: A set of sentences expressed in a knowledge representation language.¹1. Unlike reflex agents, a knowledge-based agent can be told new facts at runtime and immediately change its behavior without needing to be re-programmed.
• Sentences represent assertions about the world (Axioms are sentences taken as true without derivation).

To act, the agent TELLs the KB what it perceives, and ASKs the KB what it should do.

Logic Terminology

• Syntax: Rules defining well-formed sentences in the language.
• Semantics: Defines the truth of a sentence with respect to each possible world (model).²2. Syntax is “how you write it”; semantics is “what it means.” “X + Y = Z” is syntactically valid math, but its semantic truth depends on the values of the variables.
• Model: A mathematically structured abstraction of the world where every sentence is either true or false.

Entailment & Inference

Entailment: KB \models \alpha (The KB entails sentence \alpha).³3. Entailment is the invisible mathematical reality; inference is the computer algorithm trying to uncover that reality.

• This means \alpha is true in every model where the KB is true.

Inference: The algorithmic process of deriving new sentences from old ones. KB \vdash_i \alpha means algorithm i derives \alpha from the KB.

• Soundness: An algorithm is sound if it only derives entailed sentences (doesn’t make things up).
• Completeness: An algorithm is complete if it can derive all entailed sentences.

Propositional Logic

A very simple logic consisting of proposition symbols (e.g., P_1, Q_2) and logical connectives.⁴4. Propositional logic is extremely limited because you cannot express general rules easily (e.g., you’d need a separate rule for every single square on a chessboard).

Connectives:

• \neg (Not)
• \land (And)
• \lor (Or)
• \implies (Implies)
• \iff (If and only if)

Theorem Proving

Checking entailment can be done by:

1. Model Checking: Enumerating all possible truth assignments and checking if \alpha holds whenever KB holds (Truth tables). O(2^n) time.
2. Inference Rules: Applying sound rules directly to sentences.
   • Modus Ponens: If \alpha \implies \beta and \alpha, then \beta.
   • And-Elimination: If \alpha \land \beta, then \alpha.

Resolution

A powerful, single inference rule that is sound and complete for propositional logic.⁵5. Because resolution is complete, we can use it to build automated theorem provers that guarantee a definitive answer.

Requires sentences to be in Conjunctive Normal Form (CNF) (an AND of ORs).

Rule: l_1 \lor ... \lor l_k and m_1 \lor ... \lor m_n, where l_i and m_j are complementary literals (e.g., P and \neg P).

Resolve to: l_1 \lor ... \lor l_{i-1} \lor l_{i+1} \lor ... \lor l_k \lor m_1 \lor ... \lor m_{j-1} \lor m_{j+1} \lor ... \lor m_n.

DPLL Algorithm

DPLL is a complete, backtracking-based search algorithm for deciding propositional satisfiability (SAT). It improves on pure model checking through three powerful heuristics:

1. Early Termination: The algorithm stops evaluating a clause if any literal is already satisfied, and stops evaluating the entire formula if any clause is already falsified.
2. Pure Symbol Heuristic: If a symbol appears with only one sign (either strictly positive or strictly negative) throughout all clauses, DPLL assigns it the value that satisfies all those clauses.
3. Unit Clause Heuristic: If a clause has only one unassigned literal left (and all others are false), that literal must be assigned true for the formula to be satisfied, forcing an immediate assignment.