Input · Notation3
Output
Reading a verdict
- INCONSISTENT · ENTAILED · UNSATISFIABLE — sound: a proof; it holds however the open world is extended.
- consistent · NOT ENTAILED · SATISFIABLE — only “no refutation in the lowered fragment”; a constraint z3 could not model may make it a false positive.
undetermined— z3 returnedunknown(undecidable fragment or timeout).
juliett lowers your document to what z3 can decide, and lowering only ever drops detail — never adds it. So refutations survive, but “a model exists” answers are relative to what was lowered. Trust the sound side outright; read the other as not yet refuted.
Semantics · what tarski / una / herbrand mean
| flag | distinct names? | distinct existentials? | reading | enrico |
|---|---|---|---|---|
| tarski (default) | no — may co-refer | may coincide | pure classical FOL / RDF Surfaces spec | refused* |
| una | yes | may coincide | classical + unique names | NOT ENTAILED |
| herbrand | yes | yes — distinct | standard names (what EYE computes) | ENTAILED |
herbrand = una + “distinct existentials are distinct too.”
*tarski has no unique-name assumption, so log:notEqualTo on variables has no
faithful image and is refused. The distinction is only observable through the equality builtins
(log:equalTo/notEqualTo, owl:sameAs/differentFrom);
on an equality-free document all three agree. Load the enrico example above and
toggle the Semantics radio to watch the verdict flip.
arg-modes (with the query verb): the operational reading —
a rule whose builtin has an unbound required input can never fire, so it is dropped before lowering,
the way a saturation reasoner evaluates. A syntactic pre-filter outside z3, and a fourth knob
alongside the three readings above. To mimic mainstream N3 reasoners such as EYE, select
herbrand + arg-modes.
The reasoning core is the same Go code as the native juliett CLI, compiled to
GOOS=js GOARCH=wasm; only the solver seam differs (the CLI shells out to a native z3,
this page calls an in-browser z3). See web/z3.js for how to host z3 on a static site.