Differentiable modal logic, in PyTorch.

Necessity (□), possibility (◇), and Kripke worlds — as tensors with gradients. Learn accessibility relations end-to-end; reason over what is, what must be, and what could be.

$ pip install torchmodal

View on GitHub →

What it gives you

□

Necessity

Compute □φ over accessible worlds. Soft- and hard-relaxations, both differentiable.

◇

Possibility

Dual to □. Existential reasoning, branching futures, or an attention readout.

[L,U]

Learnable bounds

Each proposition gets a learnable interval per world — support and plausibility, end-to-end.

≠

Contradiction loss

Penalise L > U, neighbour disagreements, and broken axioms. Coherent under gradient descent.

Use case · Multi-agent control

Control multi-agent systems via learned accessibility.

Treat each agent as a Kripke world. The accessibility relation R becomes a learnable communication graph — who sees whom, and how strongly. Each proposition carries a learnable interval [L, U] of truth at every world; necessity (□) reads as consensus, possibility (◇) as any-neighbour signal, and a contradiction loss keeps the assignments coherent. Backprop through all three to discover the topology and the truth bounds that solve the task.

Interval propositions — every proposition gets a learnable [L, U] per world; L = support, U = plausibility. Tight intervals mean confidence; wide ones mean ignorance.
Decentralised consensus — □safe holds only when every agent an agent communicates with believes it.
Sparse coordination — regularise R with an L1 penalty; the model learns who needs to talk to whom.
Contradiction loss — penalise L > U, neighbour disagreements, and violated axioms (T, K, 4…) so beliefs stay logically coherent under gradient descent.

# Four agents, fully-connected init.
# Learn a sparse R, learn [L, U] per proposition, keep beliefs coherent.
from torchmodal import KripkeModel, ops, losses

agents = KripkeModel(num_worlds=4, num_props=8,
                     learn_R=True, learn_bounds=True)

# Per-world, per-proposition interval [L, U]. Both ends are learnable.
L, U  = agents.bounds("safe")        # shape: (num_worlds,)

# □safe — consensus across each agent's neighbours, on both bounds
box_L = ops.necessity(L, agents.R)
box_U = ops.necessity(U, agents.R)

task_loss     = control_objective((box_L, box_U), target)
sparse_loss   = agents.R.abs().mean()           # prune unused channels
contra_loss   = losses.contradiction(agents)    # L > U, axiom violations,
                                                # neighbour disagreement

(task_loss + 1e-2*sparse_loss + 1e-1*contra_loss).backward()

A taste

# Two worlds, learned accessibility, interval [L, U] per proposition.
from torchmodal import KripkeModel, ops, losses

model = KripkeModel(num_worlds=2, num_props=4,
                    learn_R=True, learn_bounds=True)

L, U      = model.bounds("safe")            # learnable [L, U] per world
box_L     = ops.necessity(L, model.R)         # □ lower bound
box_U     = ops.necessity(U, model.R)         # □ upper bound

task      = ((box_L + box_U)/2 - target).pow(2).mean()
contra    = losses.contradiction(model)       # keep beliefs coherent

(task + 0.1 * contra).backward()