human + your own LLM · real Z3, in this tab · consistency, not truth

The shape of a
world-model’s disagreement.

Hold a set of claims. This tool never parses them — your LLM turns each into a typed logical IR (you confirm the plain-English render, never syntax). Then a real solver computes not a yes/no but the whole dialectic: every coherent position the claims admit, every irreducible disagreement between them, and the least-entrenchment way out. The trajectory is the object; the conflict is its structure.

Add a claim What this is & isn’t Source

Trajectory

Each claim, as your sentence and its rendered logic. The colour is its dialectical standing across all coherent positions — necessary, contested, or defeated. Entrenchment is how hard it is to give up; it is yours to set.

Coherence field

Computed by Z3 in this tab — not asserted. The diagram is the conflict structure; the cards are the positions you could actually hold.

no claims yet — load the trajectory, or add one below

Trajectory tree

A world-model is not one state but a tree of them. Save the current one as a branch, fork it, retract or add a claim down one branch, and put two branches’ coherence side by side — a debate you can actually walk. Branches persist in this browser; nothing leaves the tab.

Add a claim — the formalization loop
Step 0 · optional — auto-formalize (OpenRouter, your key)

No manual round-trip: your model formalizes, the engine ingests, Z3 analyzes — in one click. This is the one path where data leaves the tab: your sentences and the current vocabulary are sent to OpenRouter under your key (stored only in this browser). The same honest seam still holds — you confirm each plain-English render; nothing is taken on faith.

Step 1 · or formalize by hand with any LLM
Step 2 · paste the IR back

Typed IR, not solver syntax. Malformed IR or type errors are surfaced verbatim — never silently guessed. Each claim then appears as plain English you confirm.

What this is — and what it is not

The seam is the point — three places this is honest about, none hidden:
  1. NL → IR faithfulness is you + your LLM, in the open. You confirm the rendered English, never logic. The tool guarantees consistency of the formalization, never that it captures your sentence. That stays yours.
  2. Z3 can answer unknown (or the IR can be ill-formed) on hard fragments. That is surfaced as undecided — never a verdict, never silently “consistent”.
  3. Enumeration is exhaustive (the MARCO algorithm — no claim-count cap), bounded only by an honest budget on pathological cases. If the budget is hit it says “real but not exhaustive” — it never silently truncates the lattice.
Goal: consistency, not truth. It never claims your claims are right — only which subsets can hold together (the dialectic), which can’t (the irreducible disagreements), the least-entrenchment way out, and what you’re jointly committed to.

A truth-maintenance system + AGM belief revision, made legible (Doyle / de Kleer / Alchourrón–Gärdenfors–Makinson; minimal conflicts & their hitting-set–dual correction sets, Reiter / Liffiton–Sakallah; defaults & the specific-over-general via Poole specificity + Brewka preferred subtheory). A Rust core (wmt-core, wasm) owns the typed IR, the IR↔SMT compiler, the English renderer, the trajectory, the full MARCO conflict/position enumerator, the defeasible and Dung-argumentation readings and the forkable-branch (de)serialization — it does not solve. The solver is Z3 4.16 (wasm), here in your tab. The compiler, MARCO enumeration (every minimal conflict and maximal coherent position, no claim-count cap), Reiter duality, the min-entrenchment repair, explanation witnesses, the defeasible layer, the argumentation framework, symbol auto-declaration and the branch round-trip are verified end-to-end against the native Z3 binary — 27 tests, incl. a quantified contradiction, an arithmetic one, MARCO past the old cap, the MUS↔MCS duality cross-check, plus a real-browser headless run of the whole stack in CI. First load fetches ~34 MB of Z3 wasm, then it is cached.