Skip to content

Reasoning

Differentiable forward chaining over a propositional Horn knowledge base: declare facts and rules in a PropKB, then run a ForwardChainer to the deductive closure. The premise conjunction is a product t-norm (a Pi neuron — see Logic), so chaining is differentiable in the facts.

polyweave.reasoning

Differentiable symbolic reasoning — forward chaining over a propositional KB.

Define facts and Horn-clause rules in a :class:PropKB, then run a :class:ForwardChainer to the deductive closure. The premise conjunction is a product t-norm (a Pi neuron, see :mod:polyweave.logic), so chaining is differentiable in the facts: you can backpropagate through it or embed it as a reasoning layer.

For propositional Horn clauses, forward chaining to the fixpoint is sound and complete for entailment, so a goal-directed backward chainer is not needed to answer "does the KB entail the goal?". A genuinely differentiable backward/Neural-Theorem-Prover-style prover (soft unification + proof trees) is a deliberate future addition, not required here.

ForwardChainer 

ForwardChainer(kb: PropKB, max_steps: int = 10, t_norm: str = 'product', tol: float = 1e-06)

Bases: Module

Iterate :class:ForwardChainingStep to the fixpoint (deductive closure).

Parameters:

Name Type Description Default
kb PropKB

the knowledge base.

 required
max_steps int

maximum chaining iterations (bounds reasoning depth).

 10
t_norm str

"product" or "min".

 'product'
tol float

stop early once a step changes the facts by less than this.

 1e-06
Source code in polyweave/reasoning/forward.py 
87
88
89
90
91
92
93
def __init__(self, kb: PropKB, max_steps: int = 10,
             t_norm: str = "product", tol: float = 1e-6) -> None:
    super().__init__()
    self.kb = kb
    self.max_steps = max_steps
    self.tol = tol
    self.step = ForwardChainingStep(kb, t_norm=t_norm)

forward 

forward(facts: Tensor, return_history: bool = False) -> 'torch.Tensor | Tuple[torch.Tensor, List[torch.Tensor]]'

Chain facts to the fixpoint.

Parameters:

Name Type Description Default
facts Tensor

(batch, N) initial truth vector.

 required
return_history bool

also return the per-step list of fact tensors.

 False

Returns:

Type Description
'torch.Tensor | Tuple[torch.Tensor, List[torch.Tensor]]'

The closure (batch, N), or (closure, history) if requested.
Source code in polyweave/reasoning/forward.py 
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
def forward(
    self, facts: torch.Tensor, return_history: bool = False
) -> "torch.Tensor | Tuple[torch.Tensor, List[torch.Tensor]]":
    """Chain ``facts`` to the fixpoint.

    Args:
        facts: ``(batch, N)`` initial truth vector.
        return_history: also return the per-step list of fact tensors.

    Returns:
        The closure ``(batch, N)``, or ``(closure, history)`` if requested.
    """
    history: Optional[List[torch.Tensor]] = [facts.clone()] if return_history else None
    f = facts
    for _ in range(self.max_steps):
        f_new = self.step(f)
        if return_history:
            history.append(f_new.clone())
        if (f_new - f).abs().max().item() < self.tol:
            f = f_new
            break
        f = f_new
    return (f, history) if return_history else f

entails 

entails(facts: Tensor, goal: str, threshold: float = 0.5) -> Tuple[bool, float]

Does the KB entail goal from facts? Returns (entailed, truth).

Source code in polyweave/reasoning/forward.py 
119
120
121
122
123
124
@torch.no_grad()
def entails(self, facts: torch.Tensor, goal: str, threshold: float = 0.5) -> Tuple[bool, float]:
    """Does the KB entail ``goal`` from ``facts``? Returns ``(entailed, truth)``."""
    closure = self(facts)
    truth = closure.reshape(-1)[self.kb.idx(goal)].item()
    return truth >= threshold, truth

ForwardChainingStep 

ForwardChainingStep(kb: PropKB, t_norm: str = 'product')

Bases: Module

One differentiable forward-chaining step over a :class:PropKB.

Parameters:

Name Type Description Default
kb PropKB

the knowledge base (facts + rules) to compile into frozen masks.

 required
t_norm str

"product" (default; and = prod, smooth, the Sigma-Pi form) or "min" (crisp Gödel conjunction).

 'product'
Source code in polyweave/reasoning/forward.py 
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
def __init__(self, kb: PropKB, t_norm: str = "product") -> None:
    super().__init__()
    if t_norm not in ("product", "min"):
        raise ValueError(f"t_norm must be 'product' or 'min', got {t_norm!r}")
    self.t_norm = t_norm

    N, R = kb.num_facts, kb.num_rules
    premise_mask = torch.zeros(R, N)
    conclusion_oh = torch.zeros(R, N)
    for r, (prems, concl) in enumerate(kb.rules):
        for p in prems:
            premise_mask[r, p] = 1.0
        conclusion_oh[r, concl] = 1.0
    self.register_buffer("premise_mask", premise_mask)    # (R, N)
    self.register_buffer("conclusion_oh", conclusion_oh)  # (R, N)

forward 

forward(facts: Tensor) -> torch.Tensor

Apply one chaining step. facts: (batch, N) -> (batch, N).

Source code in polyweave/reasoning/forward.py 
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
def forward(self, facts: torch.Tensor) -> torch.Tensor:
    """Apply one chaining step. ``facts``: ``(batch, N)`` -> ``(batch, N)``."""
    f = facts.unsqueeze(1)              # (batch, 1, N)
    mask = self.premise_mask            # (R, N)

    # Set non-premise positions to 1 (neutral for both product and min), so the
    # reduction sees only the rule's premises.
    masked = f * mask + (1.0 - mask)    # (batch, R, N)
    if self.t_norm == "product":
        fire = masked.prod(dim=-1)      # (batch, R)
    else:
        fire = masked.min(dim=-1).values

    # OR the rule activations onto their conclusion facts.
    derived = (fire.unsqueeze(-1) * self.conclusion_oh).max(dim=1).values  # (batch, N)
    return torch.max(facts, derived)

PropKB 

PropKB()

A propositional knowledge base: named facts + Horn-clause rules.

Example

kb = PropKB() kb.add_rule(["raining"], "wet_grass") # raining -> wet_grass kb.add_rule(["wet_grass"], "slippery") # wet_grass -> slippery kb.add_rule(["wet_grass", "sunny"], "rainbow") # a conjunction f0 = kb.initial_facts(["raining"]) # (1, N) truth vector

Source code in polyweave/reasoning/kb.py 
29
30
31
32
def __init__(self) -> None:
    self._fact_index: Dict[str, int] = {}
    self.rules: List[Tuple[List[int], int]] = []   # (premise_indices, conclusion_idx)
    self.rule_names: List[str] = []

fact_names property 

fact_names: List[str]

Fact names in index order.

add_fact 

add_fact(name: str) -> int

Register name (idempotent) and return its integer index.

Source code in polyweave/reasoning/kb.py 
36
37
38
39
40
def add_fact(self, name: str) -> int:
    """Register ``name`` (idempotent) and return its integer index."""
    if name not in self._fact_index:
        self._fact_index[name] = len(self._fact_index)
    return self._fact_index[name]

idx 

idx(name: str) -> int

Integer index of a registered fact (raises KeyError if unknown).

Source code in polyweave/reasoning/kb.py 
51
52
53
def idx(self, name: str) -> int:
    """Integer index of a registered fact (raises ``KeyError`` if unknown)."""
    return self._fact_index[name]

initial_facts 

initial_facts(true_facts: List[str]) -> torch.Tensor

A (1, N) truth vector with 1.0 at each name in true_facts.

Source code in polyweave/reasoning/kb.py 
55
56
57
58
59
60
def initial_facts(self, true_facts: List[str]) -> torch.Tensor:
    """A ``(1, N)`` truth vector with ``1.0`` at each name in ``true_facts``."""
    f = torch.zeros(1, self.num_facts)
    for name in true_facts:
        f[0, self.idx(name)] = 1.0
    return f

add_rule 

add_rule(premises: List[str], conclusion: str, name: str = '') -> None

Add a Horn clause and(premises) -> conclusion.

All names are auto-registered as facts. name is an optional human label (defaults to a rendered "a, b -> c").

Source code in polyweave/reasoning/kb.py 
64
65
66
67
68
69
70
71
72
73
74
75
76
def add_rule(self, premises: List[str], conclusion: str, name: str = "") -> None:
    """Add a Horn clause ``and(premises) -> conclusion``.

    All names are auto-registered as facts. ``name`` is an optional human label
    (defaults to a rendered ``"a, b -> c"``).
    """
    for p in premises:
        self.add_fact(p)
    self.add_fact(conclusion)
    prem_indices = [self.idx(p) for p in premises]
    concl_index = self.idx(conclusion)
    self.rules.append((prem_indices, concl_index))
    self.rule_names.append(name or (", ".join(premises) + " -> " + conclusion))

describe 

describe() -> None

Print a short summary of facts and rules.

Source code in polyweave/reasoning/kb.py 
82
83
84
85
86
87
def describe(self) -> None:
    """Print a short summary of facts and rules."""
    print(f"Facts ({self.num_facts}): {self.fact_names}")
    print(f"Rules ({self.num_rules}):")
    for i, name in enumerate(self.rule_names):
        print(f"  R{i}: {name}")

print_facts 

print_facts(facts: Tensor, kb: PropKB, threshold: float = 0.5) -> None

Print each fact's truth value, ticking those at/above threshold.

Source code in polyweave/reasoning/forward.py 
127
128
129
130
131
132
def print_facts(facts: torch.Tensor, kb: PropKB, threshold: float = 0.5) -> None:
    """Print each fact's truth value, ticking those at/above ``threshold``."""
    f = facts.reshape(-1)
    for name in kb.fact_names:
        v = f[kb.idx(name)].item()
        print(f"  {'[x]' if v >= threshold else '[ ]'} {name:<22s} {v:.4f}")