The Zizkian logic checker
Try the editable browser lab. It runs this same module using SWI-Prolog WebAssembly in a worker. Records stay in the tab; the lab does not call a model or submit records to a server. Browser input is bounded to 64 KiB, 20 nested levels and 500 entries per array, with a five-second execution timeout. The native CLI does not impose these browser resource limits.
Run from the repository root with SWI-Prolog installed:
swipl -q -s src/check.pl -- examples/hypothesis.json
swipl -q -s tests/test_zizkian.pl -g run_tests -t halt
swipl -q -s proof/refutable.pl
The checker reads JSON as data. It does not execute supplied Prolog, call models,
fetch sources, change files or send messages. The native CLI uses the installed
SWI-Prolog; the browser lab bundles a separately licensed WASM runtime.
Its public predicates are zizkian:audit/2, zizkian:audit_json/2 and zizkian:audit_file/2.
?- use_module('src/zizkian.pl').
?- audit_file('examples/defeated.json', Report).
audit_json/2 accepts a JSON text atom or string. Native files must be valid UTF-8;
byte validation rejects overlong encodings and invalid Unicode scalar values
before a decoder can repair them. The shared JSON entry rejects syntax extensions,
duplicate object keys, a leading BOM and isolated Unicode surrogate escapes.
Valid surrogate pairs, ordinary Unicode and escaped control characters are
accepted. JSON text fields must be strings, invitations must be actual Booleans,
and status fields must contain one of the named strings. Parsing retains types
until schema validation; the text "false" cannot become an invitation Boolean.
Native files and the browser worker call this same predicate.
Valid supplementary-character escapes are normalized before the library parses
them, including on older SWI-Prolog libraries without surrogate-pair support.
Literal backslashes remain literal, and malformed pairs remain invalid.
audit/2 is the direct Prolog API: it accepts a ground dict with atom text values
and grounded dict tags. It has no knowledge of the original JSON encoding.
Do not convert unvalidated JSON strings to atoms yourself: use audit_json/2
or audit_file/2 at a JSON boundary.
Do not pass variables to mean unknown. Use hypothesis, untested and unasked.
Missing, blank, mistyped and unrecognized fields are invalid; there are no silent
defaults. Evidence and reading IDs must be unique, and references must resolve.
| Exit | Status | Meaning |
|---|---|---|
| 0 | pass |
Record satisfies these encoded rules; warnings may remain |
| 1 | blocked |
Valid input violates one or more reasoning rules |
| 2 | invalid |
Repair input, schema, references or invocation |
Passing verdicts are awaiting_closure_review, awaiting_test_review and awaiting_change_review.
They request review of the declared outcome; none authorizes an action. Every
report, including errors, contains scope: "declared_record_only",
evidence_verified: false, schema_version: "0.3.2" and human_review_required.
That list covers source authenticity, relevance, test discrimination, the ordinary
alternative’s strength, participant authority, analyst payoff and the decision
to stop. It lists work still required, not checks that the program performed.
Every violation contains rule, target and message. All detected violations
are returned, rather than stopping at the first one. Warnings preserve explicitly
untested alternatives and falsifiers.
Record contract
All listed fields are required. See the complete examples rather than inventing
an incomplete record. schema/2 in zizkian.pl is the executable schema.
The downloadable JSON shape schema is generated
from schema/2. It describes field types and status vocabularies, not nonblank
text, reference validity or reasoning constraints. Use the checker for those.
| Object | Fields |
|---|---|
| Case | id, mode, coaching_invited, brief, desired_result, owner, lenses, ordinary, return_cut, evidence, readings, outcome |
| Ordinary alternative | claim, check, status (untested or checked), evidence IDs |
| Return cut | observer, statement, defeater, status (hypothesis or no_finding) |
| Evidence item | id, statement, source, kind (observation, participant_rejection or attention_weight) |
| Reading | id, claim, status (hypothesis, supported or withdrawn), response (unasked, accepted or rejected), support IDs, counterevidence IDs, defeat_test |
| Defeat test | method, defeating observation, status (untested, survived or defeated), evidence IDs |
| Outcome | kind (retain_brief, test or change), action, reason, reading_ids, stop_rule |
supported is a declared epistemic status, not a conclusion generated by this
program. Likewise, survived means the submitted record declares that the test
did not defeat the reading; it does not mean the reading is universally true.
Consulting uses 1 to 3 distinct business lenses, optionally including veil_piercer.
Coaching uses one personal lens or veil_piercer, requires invitation and an
accepted framing for a selected next step. Rejection cannot support any active
reading, and a rejected framing cannot drive the participant’s next step.
An active supported reading needs observation evidence and no unresolved declared counterevidence. The same item cannot count as support and counterevidence. Defeated readings must be withdrawn. Observed test results and checked ordinary alternatives require an observation reference. A change requires a checked ordinary alternative and supported selected readings. A test may select a hypothesis. Closure uses no selected reading and permits withdrawal.
Runnable examples
Every example is fictional, including its evidence and participant statements.
| Input | Expected status | Why |
|---|---|---|
| hypothesis.json | pass / awaiting_test_review, warnings | A test is proposed without claiming an observed result |
| supported.json | pass / awaiting_change_review | Declared support, alternative check and test record are present |
| defeated.json | blocked | Reading remains active after its defeating observation |
| withdrawn.json | pass / awaiting_closure_review | Withdrawal permits closure |
| no-finding.json | pass / awaiting_closure_review | An ordinary answer needs no dramatic reading |
| rejection-trap.json | blocked | Rejection is used as evidence and the refused framing drives a step |
| false-evidence.json | pass / awaiting_change_review | Deliberately irrelevant prose still has a structurally valid reference |
| plausible-fabrication.json | pass / awaiting_change_review | A deliberately invented study cannot be authenticated by these rules |
| self-sealing.json | pass / awaiting_change_review | A deliberately invalid test treats disclosure and nondisclosure as confirmation; human review must reject it |
| self-sealing-withdrawn.json | pass / awaiting_closure_review | Withdraw the unsupported reading while preserving observations and an unknown internal cause |
| incomplete.json | invalid | Missing owner is a schema error |
Scope and limitations
This checks the structure and declared relationships of a reasoning record.
It cannot judge whether a sentence actually supports another sentence, a source
exists, a test was honestly performed, consent was real, or a falsifier is strong.
Mislabelled rejection as observation can evade a type check. Arbitrary prose can
fill every required field. Human evidence review remains necessary.
The self-sealing pair makes test discrimination inspectable. Run both records;
the first passes despite its test being unable to lose, and the second closes
without claiming a hidden draft or proving its absence. Declaring survived
does not make a test valid. The portable warnings are in existing text fields;
adding an unrecognized note field would instead make the input invalid.
Their declared outcomes produce different review labels; this does not mean
the program has judged one test better. Human review rejects the first test.
Withdrawal fits this unsupported claim. A supported reading with a genuinely
discriminating test can remain active, as the ordinary supported example shows.
Negation-as-failure is used only after input validation: missing support in the record blocks a supported claim. It does not prove that no support exists in the world. No attention weights, confidence score or voting arithmetic are applied. Changing a lens cannot change the supplied evidence.
The checker is available for manual use. It is not automatically connected to a dispatcher. See the field guide.
Method coverage
| Method commitment | Encoded check | Human responsibility |
|---|---|---|
| Preserve the question and owner | Nonblank brief, desired_result, owner |
Confirm this is the participant’s strongest intended question |
| Consider an ordinary explanation | Required alternative; checked needs an observation before change |
Check that it is strong, relevant and fairly tested |
| Select useful lenses | Permitted names, distinct names, mode and count | Decide relevance and whether questions actually differ |
| Put a reading at risk | Required defeat method and observation; declared defeat blocks an active reading | Judge whether the test could discriminate or was honestly run |
| Apply the return cut | Required observer, statement, defeater and status | Inspect payoff and record its consequence in outcome.reason and action |
| Respect participant authority | Invitation Boolean; selected coaching framing must be accepted; rejection traps blocked | Establish real invitation, consent and authority to act |
| Stop or change direction | Outcome basis and status relationships | Decide when another pass changes no useful test or decision |
No encoded rule connects the return cut to the outcome or enforces a historical recursion limit. The checker audits one snapshot, not the conversation. The method’s return-cut worksheet is human work. Two different names in fields would not establish independence.
Migrating from 0.2.0
Input field names and status vocabularies are unchanged. Inputs that relied on string Booleans, literal control characters, trailing commas or a BOM are now invalid. Serialize valid JSON instead of relying on parser extensions.
| Old passing verdict | 0.3.2 verdict |
|---|---|
no_finding |
awaiting_closure_review |
ready_for_test |
awaiting_test_review |
ready_for_decision |
awaiting_change_review |
Exit codes and status values are unchanged. Consumers must tolerate the report
metadata and keep its scope visible when displaying or forwarding a result.
The implementation uses SWI-Prolog’s documented JSON dict interface and PlUnit.
Treat structural passage as a review aid [1 SPECULATIVE | no outcome benchmark]. If that use is wrong, the first signal is a misleading record passing despite a human reviewer finding unsupported conclusions or an unusable defeating test.