A knowledge-based agent stores facts as sentences in a formal language and derives new facts by inference. Propositional logic is the simplest such language: sentences are built from true/false symbols with connectives.

TELL the KB what is perceived → ASK the KB what to do (inference) → TELL the KB the action taken

Syntax and semantics

Connective	Symbol	Read as	True when
Negation	`¬P`	not P	`P` is false
Conjunction	`P ∧ Q`	P and Q	both are true
Disjunction	`P ∨ Q`	P or Q	at least one is true
Implication	`P ⇒ Q`	if P then Q	`P` is false or `Q` is true
Biconditional	`P ⇔ Q`	P if and only if Q	both have the same value

Key vocabulary

Term	Meaning
Model	An assignment of true/false to every symbol — a possible world
Entailment `KB ⊨ α`	`α` is true in every model where the KB is true
Inference `KB ⊢ α`	An algorithm derives `α` from the KB
Sound	Derives only entailed sentences (never lies)
Complete	Can derive every entailed sentence
Valid (tautology)	True in all models: `P ∨ ¬P`
Satisfiable	True in at least one model; unsatisfiable = true in none

Inference by model checking

The simplest sound and complete method: enumerate every model (a truth table) and check that α holds wherever the KB holds. KB: If it rains the grass is wet (R ⇒ W), the sprinkler is on or it rains (S ∨ R), the sprinkler is off (¬S).

Python

from itertools import product

SYMBOLS = ["R", "S", "W"]
implies = lambda a, b: (not a) or b
KB = [lambda m: implies(m["R"], m["W"]),
      lambda m: m["S"] or m["R"],
      lambda m: not m["S"]]

def entails(kb, query):
    models = [dict(zip(SYMBOLS, values)) for values in product([False, True], repeat=len(SYMBOLS))]
    kb_models = [m for m in models if all(sentence(m) for sentence in kb)]
    return all(query(m) for m in kb_models), len(models), len(kb_models)

print(entails(KB, lambda m: m["W"]))        # (True, 8, 1) ← KB ⊨ W: in the only KB-model the grass is wet
print(entails(KB, lambda m: m["S"]))        # (False, 8, 1)

valid = lambda f: all(f(*v) for v in product([False, True], repeat=2))
print(valid(lambda p, q: implies(p, q) == implies(not q, not p)))    # True ← contraposition is valid
print(valid(lambda p, q: implies(p, q) == implies(q, p)))            # False ← the converse is not

Model checking is exact but costs O(2ⁿ) for n symbols. Real systems use theorem proving (inference rules) or SAT solvers, which search the models cleverly.

Standard equivalences

Name	Equivalence
Implication elimination	`P ⇒ Q ≡ ¬P ∨ Q`
Contraposition	`P ⇒ Q ≡ ¬Q ⇒ ¬P`
Biconditional elimination	`P ⇔ Q ≡ (P ⇒ Q) ∧ (Q ⇒ P)`
De Morgan	`¬(P ∧ Q) ≡ ¬P ∨ ¬Q`, `¬(P ∨ Q) ≡ ¬P ∧ ¬Q`
Double negation	`¬¬P ≡ P`
Distributivity	`P ∨ (Q ∧ R) ≡ (P ∨ Q) ∧ (P ∨ R)`

Inference rule	From	Infer
Modus ponens	`P ⇒ Q`, `P`	`Q`
Modus tollens	`P ⇒ Q`, `¬Q`	`¬P`
And-elimination	`P ∧ Q`	`P`
Resolution	`P ∨ Q`, `¬Q ∨ R`	`P ∨ R`

What is the difference between entailment and inference?

How do you check whether KB entails α?