Goal Trees and Deduction in Logic

The Simplest Explanation

Searching for a proof is searching in an AND-OR graph:

• To prove $P \land Q$ → prove P and prove Q (AND node)
• To prove P when several rules each conclude P → try any one rule (OR node)

So the same AO*/goal-tree machinery from planning solves theorem proving.

Foundations

Given a knowledge base $KB$ (sentences assumed true) and a query $\alpha$:

The canonical inference rule, modus ponens: from $\alpha$ and $\alpha \Rightarrow \beta$, derive $\beta$. Content-independent — swap Man/City, Socrates/Chennai and the syllogism still works.

Forward Chaining (data-driven)

Start from KB; repeatedly apply inference rules; add conclusions; stop when $\alpha$ appears (or nothing new derives). Natural-deduction style — derives everything it can, useful when many queries are expected.

Backward Chaining (goal-driven)

Start from the goal α; find rules whose consequent matches α; recurse on their antecedents. Produces an AND-OR tree — deductive retrieval. Efficient when only one query matters.

With Variables (existential goals)

"Is someone mortal?" = prove $\exists z.\,\text{Mortal}(z)$:

1. Match goal Mortal(z) against rule $\text{Man}(x) \Rightarrow \text{Mortal}(x)$
2. Unify: substitute x = z → subgoal Man(z)
3. Match against facts: z = Socrates? Plato? …
4. Each successful full substitution yields a witness

Conjunctive Antecedents = AND Nodes

Rule: $\text{Green}(x) \land \text{Circular}(x) \Rightarrow \text{NiceToy}(x)$.

Proving NiceToy(z) requires proving Green(z) and Circular(z) — an AND node. Multiple rules concluding the same predicate are OR alternatives.

Worked Example: Nice Toys

Rules:

• R1: Green(x) ∧ Circular(x) ⇒ NiceToy(x)
• R2: Red(x) ∧ Square(x) ⇒ NiceToy(x)

Facts: Green(A), Green(B), Circular(C), Red(C), Red(D), Square(D), Circular(E)

Backward chain NiceToy(z):

• Via R1: z=A has Green(A) ✓ but Circular(A)? ✗. z=C: Circular ✓ but Green(C)? ✗. No solution via R1.
• Via R2: z=D: Red(D) ✓ and Square(D) ✓ → D is a nice toy.

This AND-OR exploration — descend promising branches, back up failures — is precisely what AO* automates with costs attached.

Properties