# PLN Backward Chaining with Multi-Path Revision (v7_multi)## Overview
A pure-MeTTa backward chainer that proves goals by recursively searching for supporting premises, computes truth values via deduction, and fuses independent proof paths via revision. Validated on PeTTa 2026-04-23.
## Architecture Layers
1. **Truth Value Arithmetic** — tv-ded-f (f1*f2), tv-ded-c (f1*f2*c1*c2)
2. **Revision** — rev-w converts confidence to weight; rev-tv fuses two tv-leafs via weighted average
3. **Base Case** — pln-bc-tv matches goal directly against &self at depth Z
4. **Recursive Step** — pln-bc-tv at depth (S d) finds intermediate $m, recurses on subgoal, applies tv-ded
5. **Multi-Path Aggregation** — MeTTa nondeterminism yields all proof paths; rev-tv fuses them
## Results (PeTTa 2026-04-23)
- **Bird-path**: Robin→Bird→Animal → (tv-leaf 0.855 0.69255)
- **Pet-path**: Robin→Pet→Animal → (tv-leaf 0.72 0.4913)
- **Revised**: rev-tv fuses both → (tv-leaf 0.8145 0.7629)
- Revision correctly weights Bird-path higher (w1≈2.253 vs w2≈0.966) due to stronger confidence
## Design Decisions
- **Peano depth control** prevents infinite recursion without external loop detector
- **Nondeterministic matching** via MeTTa semantics — all valid intermediate nodes $m are explored automatically
- **Hardcoded rev-tv call** for now; future: collapse-ndet wrapper to auto-aggregate all paths
- **Independence assumption** in revision — LLM oversight layer should flag correlated evidence sources
## Limitations & Future Work
- rev-tv currently called manually on two paths; needs automatic nondeterminism collapse
- Depth (S Z) only explores 1-hop chains; deeper trees need (S (S Z)) etc.
- No backward goal decomposition yet (splitting conjunctive goals)
- MeTTaIL compilation could auto-optimize branch traversal (Kevin's insight 2026-04-23)
- Independence detection needed before revision (correlated evidence → invalid fusion)
## V8: Automatic Nondeterminism Collapse (03:40 UTC)
V8 eliminates manual multi-path revision by using collapse to gather all nondeterministic pln-bc-tv results into a list, then fold-rev with car-atom/cdr-atom iteratively applies rev-tv. Result: (tv-leaf 0.8111 0.7694) — automatic fusion of Bird-path and Pet-path without hardcoded path knowledge. Key pattern: (= (pln-bc-revised $goal $depth) (let $paths (collapse (pln-bc-tv $goal $depth)) (fold-rev (car-atom $paths) (cdr-atom $paths)))). Code: https://nonlanguage.dev/MeTTaSoul/mb/pln_bc_v8_revised.metta
### Kevin Insight: ECAN vs Engineering Stack. Kevin observed that Pathmap+MORK+ASI chain are engineering solutions; a leaner composite uses ECAN over distributed atomspace with attention-driven shard specialization. The fold-rev pattern is associative/commutative, enabling order-independent distributed evidence fusion across specialized reasoning shards.
### V8 Depth-2 Test (03:46 UTC). 3-hop auto-collapse confirmed: !(pln-bc-revised (Inheritance Sparrow Animal) (S (S Z))) produces (tv-leaf 0.6863 0.5128), fusing Sparrow->Robin->Bird->Animal and Sparrow->Robin->Pet->Animal paths automatically. Confidence drops from 0.77 (depth 1) to 0.51 (depth 2) as expected from deduction confidence multiplication across 3 hops. Pattern generalizes: fold-rev+collapse works at arbitrary depth. Code: https://nonlanguage.dev/MeTTaSoul/mb/pln_bc_v8_depth2.metta