Ask the right question. Get the answer. Understand the reason. Run the check.
ARC turns a precise question into a portable, executable artifact that answers it, explains the derivation, and checks the result through a route capable of finding errors. This page is that pattern written in EyeProlog’s own terms, where the artifact is an ordinary Prolog program, the reason is ordinary Prolog data, and the check is a command.
Answers are cheap. Trustworthy answers are not.
A rule engine that returns true has told you that some search succeeded. It
has not told you which rules fired, which facts they rested on, or whether the
arithmetic along the way was right. In most workflows verification is a manual
afterthought: read the output, redo the calculation by hand, ask whoever wrote
the rules.
EyeProlog moves that work into the artifact:
typical workflow program → answer → someone checks it by hand
EyeProlog program → answer + proof → checked mechanically
This puts the valuable human work upstream — stating the question precisely, choosing the facts, writing the rules honestly — and leaves the mechanical work to something that can be run again tomorrow.
An answer does not become trustworthy by being emitted confidently. It becomes trustworthy by being inspectable, repeatable, and able to be shown wrong.
Every arc starts from three explicit inputs, and in EyeProlog all three live in one file:
%% ?- ageAbove(X0, X1).birthDay(patH, '1944-08-21').ageAbove(S, A) :- birthDay(S, B), ..., F @> A.From those it produces three outputs:
INPUT OUTPUT
Question ─┐ ┌─ Answer what follows
Data ─────┼─→ EyeProlog ───────┼─ Reason why it follows
Logic ────┘ └─ Check whether that why holds
Run against examples/age.pl, the three are three commands:
eyeprolog examples/age.pl # Answer
eyeprolog --proof examples/age.pl # Reason
eyeprolog examples/age.pl --check-proof examples/proof/age.pl # Check
ageAbove(patH, 'P80Y').
condition('C5', re_decision, ok, 2).
verdict(checked).
All three outputs are Prolog. The answer is a term, the proof is a set of
step/4 facts, and the check result is a set of condition/4, failure/3,
obligation/3 and verdict/1 facts — so each stage can be read by the next
one rather than only by a person.
The question is part of the specification, not a prompt. %% ?- ageAbove(X0, X1).
is precise enough to distinguish a right answer, a wrong answer, and a right
answer to a different question — and it stays in the file, so the artifact
carries what it was asked.
Nothing here is trapped in a session. The program is a text file, the proof is a text file of ordinary Prolog facts, and the check is a process exit status.
An explanation is not verification. A convincing explanation can be produced for a wrong result, so the check must be capable of disagreeing with the answer.
A proof document is read as a claim, not believed. --check-proof tests seven
conditions, specified in SPEC.md:
| condition | what it establishes | |
|---|---|---|
| C1 | Resolution | every checked step really is an instance of the clause it cites — and the clause is taken from the program, not from the document, so a proof cannot be made valid by restating the rule it used |
| C2 | Well-founded | following what a step used never leads back to it; a proof that rested on itself would prove anything |
| C3 | Justification | every step carries exactly one known justification, in the shape it requires |
| C4 | Coverage | every claim has a step, and every use resolves to a step or to an instance of a program fact |
| C5 | Re-decision | a step the document only asserts is computed again, independently, and must agree; a control step must be composed of its uses |
| C6 | Boundary consistency | a \+ or findall/3 taken on trust is confronted with the evidence the program and the document show, which can refute it |
| C7 | Relevance | every claim answers a goal that was asked, and every step serves a claim |
C5 is the trust contract. The largest class of steps in a typical proof is the primitive — arithmetic, comparison, string and date operations that no clause derives. Reading a document cannot tell whether those are true, so they are run again against a program holding the bundled libraries and nothing else. No clause of the theory under proof is present, which means the recomputation cannot be talked into agreeing by the very rules it is auditing.
This is ARC’s “genuinely different route”, made concrete: not a second implementation of the same reasoning, but the same primitive decided by a process that has been denied the theory.
The difference is not theoretical. A document can pass C1 through C4 completely — every step a proper instance, every use accounted for, no cycles — and still record a computed value that is simply false, provided it tells the same lie throughout. Only recomputation catches that one. There is a regression test that constructs exactly such a document and requires the checker to reject it, with C5 as the only objecting condition.
A condition that cannot fail is not much of a check.
Not every step needs recomputing to be established. A control construct such as
once(G) is recorded as a control step whose uses are the goals it wraps,
and those goals are themselves steps which C1 and C4 already check, so the
conclusion is carried rather than trusted — and C5 verifies that the uses are
exactly what the construct wraps instead of assuming it.
Constructs that claim something about the absence of solutions — \+ G and
findall/3 — cannot be proved by any recorded use, so they stay trusted. They
are not left unexamined, though: C6 confronts each one with the evidence at
hand — the program’s facts and the document’s own steps, for predicates that
are static and pure enough for that evidence to speak — and rejects one the
evidence contradicts. What survives is reported as an obligation.
An arc need not stay isolated. Its output is the same kind of thing as its input, which is what lets arcs compose.
A proof document is not a log; it is a set of ground Prolog facts — step/4,
clause/3, and the claims themselves. That means the checked answer of one
program can be loaded as the data of the next, and a program can reason about
a proof as readily as it reasons about anything else.
program A ──→ answer + proof ──┐
program B ──→ answer + proof ──┼──→ program C ──→ answer + proof + check
facts ────────────────────-┘
The same property connects EyeProlog to the wider data world. RDF quads convert
to ordinary rdf/4 facts and back, so an arc can take RDF in, reason in
Prolog, and emit RDF out, with the proof of the middle step available for
inspection. The contract at each boundary is explicit, so a larger arc can
check not only its own result but whether the pieces compose into an answer to
the larger question.
Checking makes trust testable. It does not make computation infallible, and the checker says which is which rather than folding everything into an undifferentiated success.
Human judgment stays essential, particularly in choosing the question and deciding what evidence is enough.
Rule-driven work with explicit structure and testable correctness conditions:
That last one is the case a proof is really for. The recipient does not have to trust the engine that produced the answer — they can check the document against the program themselves, with a different copy of the checker if they like.
The pattern is not aspirational here. Every one of the 239 examples ships
with its answer, the proof of that answer, and the result of checking the
proof, and npm test re-checks all of them on every run:
| examples | 239 |
| packaged proofs | 239 |
| packaged check results | 239 |
| recorded steps | 213091 |
| verified against a source clause | 156944 |
| recomputed independently | 55460 |
| carried by the goal they wrap | 220 |
| trusted boundaries confronted with evidence | 53 |
| remaining obligations | 467 (0.2%) |
Each obligation names the conclusion it stands for, so the residue can be read
rather than only counted. Two fifths of it is one thing: a \+ step claims a
goal of the program has no proof, and no recorded use can establish an
absence. An absence the bundled libraries can decide, such as
\+ member(b, "a"), is recomputed instead. Most of the rest are aggregates
over the program, such as countall/2 and setof/3, and character I/O.
The proof directory is read from disk rather than from a list, so a document cannot be added without being checked. An unverified proof is worse than none, because it still looks like evidence.
Worth reading in order: examples/age.pl for the smallest
complete arc, examples/deontic-logic.pl for a
policy decision traced to its rules, and
examples/clpz-n-queens.pl for a proof of a
constrained search.