3μQL: three-valued fixpoint quorum logic
Choose a theory, adjust its assumptions, and inspect the evidence.
Step 1. Choose a theory
Begin with First steps, then follow Keep exploring through the curated examples.
Choosing an example loads its theory and settings immediately. Reset restores the loaded example’s defaults.
You are working on your own theory in the editor below.
View or edit the theory
Insert at the cursor · arrows browse · Enter inserts
Step 2. Choose what to test
Select the claims you want to investigate. Remove an assumption to see what changes.
Reading the theory’s properties and assumptions…
Properties
Assumptions
Step 3. Set the scope. Run the experiment.
Both modes find truth values automatically. Choose whether to search for a frame or use the one in your theory.
Preparing the example…
Step 4. Inspect the results
Read the outcome, explore a model, or download the evidence.
Your results will appear here.
Run the first example to see a small counterexample and its complete valuation.
Custom experiment — create your own theory
Ready to try your own ideas? Start a new Markdown theory, load one from your device, or return to your saved draft. Your theory opens in the same four-step workspace above.
Reset returns to the last curated example and restores its original source and settings.
Recovery copies
Separate copies keep concurrent edits safe. Restore a copy with its settings, or save its theory as a file. Up to 20 copies are kept; if storage fills, use Save theory. Forget saved draft removes this page’s draft and its recovery copies.
How to interpret the results
Counterexample found
A concrete model makes the property false while every retained axiom is satisfied. Its valuation is independently replayed before being returned.
Holds within bounds
The checker exhausted the selected scope or bounded search without finding a counterexample. This is finite evidence, not an unbounded proof.
Incomplete or inconsistent
A limit leaves the question open. If the axioms have no model in the selected scope, no property is reported as proved.
Truth values, downloads, and privacy
t means true, b means broken, and f means false. Axioms are satisfied by either t or b. A counterexample makes a property f.
Save a counterexample’s Markdown theory and JSON valuation together. Replay them with python -m muql replay theory.md countermodel.json.
Your theory and results stay on your device. Custom theories are saved as a draft in this browser when local storage is available. Each visit starts at First steps; restore your draft in Custom experiment below the results. Browsing the curated examples leaves your saved draft intact. The Python runtime loads when you first use the checker; MiniSat loads an additional package if selected. The standard online build fetches these from jsDelivr; a self-contained build can serve them with the page. There is no account or analytics. Closing the page stops computation.