Title: The EyeProlog Answer, Proof and Check Format
Version: eyeprolog 1.6.33
Status: Informational
Author: Jos De Roo, KNoWS office of IDLab, Ghent University - imec
Repository: https://github.com/eyereasoner/eyeprolog
EyeProlog runs portable ISO Prolog programs and writes their answers together with a proof whose documents a separate checker verifies against the program that produced them. This document specifies the goals a run asks, the answers it reports, the text in which answers, proofs and check reports are written and read back, the proof document, the seven conditions (C1-C7) a proof checker establishes, the check report, and the command line that ties them together.
This document is not an Internet Standards Track specification. It describes the formats as implemented by eyeprolog 1.6.33, for readers who want to produce or consume proofs and check reports, or to implement a compatible reasoner or checker. The Prolog language itself is specified by ISO/IEC 13211-1 and its corrigenda, and EyeProlog’s profile of it, its libraries and its extensions are documented in The Art of EyeProlog. Where this document and the implementation disagree, that is a defect in one of them.
An EyeProlog run asks goals of a Prolog program and reports their ground answers. Each answer can be accompanied by a proof: a document that names, for each step, the program clause, built-in or control construct that justifies it. A checker that never searches for a derivation verifies such a document against the program and reports, condition by condition, what it established and what it had to take on trust.
Answers, proofs and check reports are all ordinary Prolog facts, one term per clause. Each is something a later program can load and reason over, and none of them is ever executed when it is read.
The three outputs form an arc: the answer says what follows, the reason (the proof) says why, and the check says whether that reason holds. See ARC in EyeProlog for the motivation.
The key words “MUST”, “MUST NOT”, “REQUIRED”, “SHALL”, “SHALL NOT”, “SHOULD”, “SHOULD NOT”, “RECOMMENDED”, “MAY” and “OPTIONAL” in this document are to be interpreted as described in BCP 14 (RFC 2119, RFC 8174) when, and only when, they appear in all capitals.
true.name/arity.==); variables are identical only to themselves.(A, B), flattened left to right; a
term that is not a conjunction is its own only conjunct.A program is ISO Prolog text, read from one or more sources in the order they
are given. EyeProlog’s language profile, its bundled libraries (which a
program MAY load explicitly or have autoloaded) and its extensions are
specified in The Art of EyeProlog; with --iso-strict the profile is
ISO/IEC 13211-1 with Corrigenda 1-3 only.
A proof cites a clause by its clause number. Numbers are given to the program’s own clauses and directives, not to those of a bundled library:
module/2, use_module/1,2,
meta_predicate/1 or attribute/1 declaration takes no number;A clause number therefore depends only on the source text, never on what
assert/1 or retract/1 do while the program runs.
A run asks a sequence of goals. They are, in order of precedence:
--goal (Section 12) or to the
embedding API;%% ?- Goal., whose goal MAY continue on following lines that begin
with %%, in source order;?- Goal. queries of the program, in source order.A declared goal is a commented-out ISO query, so it reads exactly like the
?- Goal. a program may write directly, but it is inert to every other Prolog
processor. A goal is read with the program’s operators and double_quotes
flag.
Each goal is solved in turn with ISO Prolog’s execution model, after the program’s initialization goals have run. Every solution that leaves the goal ground is an answer, the goal’s instance under that solution. A solution that leaves a variable unbound is not reported.
An answer is reported, as its written text (Section 6) followed by . and a
newline, unless:
The answers of a run are its claims, in the order reported.
Answers, proofs and check reports write each term as writeq/1 would, with
the program’s operator table and its double_quotes flag in force:
'Name' included;double_quotes(chars) (the default), is written
as a double-quoted string, and a list ending in such a list is written
[a, b|"cd"];'$VAR'(N) is written as itself, not as the variable letter
writeq/1 would print for it: the letter would read back as a variable.The written text of a term MUST read back, with the same operators and flags, as a term identical to it up to the renaming of variables.
A document is read as a sequence of Prolog clauses, with the operators and
double_quotes flag of the program it is checked against. It is read as data:
a reader MUST NOT execute anything, a directive included. Within one clause a
variable name denotes one variable, and _ a fresh one each time; variables
are never shared between clauses.
When a proof is requested, each claim’s derivation is reconstructed by replaying its goal against the program until the first derivation of that claim is found, and the derivation is resolved against the final substitution of the whole derivation: each goal is recorded as it stands once the derivation is complete, not as it stood when it was solved.
The replay records how each goal was justified: by a clause of the program,
by a built-in or a bundled library predicate, by a control construct and the
goals it wraps, by an absence (\+), by a collection (findall/3), or by a
clause assert/1 added at run time.
The proof detail decides how far a derivation is explained:
abstract (the default) stops at a bundled library predicate and records
it as one builtin step;expanded explains through it, recording the library’s own clauses as
builtin steps, since they have no clause number.A claim is replayed as the ground goal it is. When that finds no derivation – typically because the program insists on computing an argument itself, as a counter, a generated name or a stream handle is computed – the goal the run asked is replayed instead, and the first derivation whose answer is the claim is recorded.
A goal Module:Goal is replayed as Goal in Module, as the solver runs it:
in a bundled library under abstract detail as one builtin step for the
qualified goal, and otherwise as a control step whose use is Goal.
A disjunction, an if-then, an if-then-else, a soft-cut and call/1 are
replayed branch by branch and recorded as a control step resting on the
branch they took. The condition of an if-then-else commits to its first
solution, as execution does. A construct that took its else branch rests on
\+ C, recorded as an absent step, and then on the goals of E: the else
branch is only taken when the condition has no solution. A condition that
tests instantiation (var/1, nonvar/1, the type tests, ==/2, \==/2,
the standard order comparisons, compare/3, \+/1) on a term that is not
yet ground is not split: its truth when tried can differ from its truth once
the derivation is complete, and the construct is one builtin step.
A derivation deeper than the replay’s nesting budget continues as a chain: each level commits to the first clause whose head matches the goal and whose body, up to a final call of a program predicate, is proved, and that final call is the next level. A chain finds the leftmost derivation – the one depth-first search finds first – whenever that derivation needs no backtracking into an earlier level, so a deterministic recursion of any depth is explained without nesting.
A claim whose derivation the replay still cannot reproduce – an answer that
depends on state the run changed, such as a counter kept in the database –
is recorded as unproven rather than left without a step. A document
containing such a step is not a valid proof (Section 9.4).
A reasoner MUST check every proof it generates, as Section 9 describes and
against the goals the run asked, before writing it, and MUST fail with an
error rather than write a proof that does not pass. The answers a run has
already reported stay reported; only the proof is withheld. A run with
unproven steps therefore fails when a proof is asked of it. A run without
claims has a proof without claims, which is valid and certifies nothing.
A reasoner MAY check the structures its proof is written from rather than reading the written document back, provided the report is the one reading the document would give.
A proof document is a document (Section 6.2) holding, in this order:
clause(N, Head, Body) per program clause the proof cites, by
increasing N;step(Goal, By, Bindings, Uses) per justified goal.A run without claims writes no proof. A checker MUST treat every fact that is
neither clause/3 nor step/4 as a claim, whatever its position.
clause(N, Head, Body) restates clause N (Section 3). Body is true for
a fact, and the clause’s body goals joined right-associatively with ,
otherwise. So that the identity of a variable survives being written into a
separate fact, each variable of the clause is written as a term:
X as var('X');_ as anonymous(I), numbered from 1 in
order of first occurrence within the record;Var#17, containing a number
that counts across the whole run) as var('Var#K'), where K numbers the
minted variables from 1 in order of first occurrence across the whole
document.Records are not authority: a checker MUST compare each with the program it checks against (Section 9.2).
Goal is the justified goal as it stands once the whole derivation is found.
Steps appear in the order a depth-first, left-to-right walk from the claims
first meets each goal; each distinct goal (by written text) has one step, and
a conjunction contributes its conjuncts rather than a step of its own. Uses
is the list of the goals that justify Goal, in order. By is one of:
By |
Meaning | Bindings |
Uses |
|---|---|---|---|
rule(N) |
Goal is an instance of the head of rule N, whose body instance is Uses. |
the clause’s variables | the body instance |
fact(N) |
Goal is an instance of fact N. |
the clause’s variables | empty |
builtin |
Goal is a built-in or bundled library goal that holds. |
empty, or a library clause’s variables under expanded |
empty, or a library clause’s body under expanded |
control |
Goal is call/1, once/1, ignore/1, catch/3, M:G, a disjunction or an if-then, solved by Uses. |
empty | the goals that solved it |
absent |
Goal is a negation \+ G taken on trust. |
empty | empty |
collected |
Goal is a findall/3 taken on trust. |
empty | empty |
asserted |
Goal was solved by a clause added at run time, which has no clause number. |
empty | empty |
unproven |
The replay could not reproduce Goal (Section 7). |
empty | empty |
Bindings is a list of 'Name' = Value pairs, one per variable of the cited
clause that the derivation bound, named as the program wrote it, in order of
first occurrence in the head and then the body; variables whose names begin
with _ are left out. A checker MUST accept any subset, since the goal and
uses determine the rest.
Minted variables and stream handles ('$stream'(I)) in steps are renumbered
in order of first occurrence across the document, as in Section 8.2, so that
the same program writes the same document on every run.
A checker is given a program, a proof document and the goals the proof answers (Section 4). It MUST NOT search for a derivation the document failed to record and MUST NOT run the program; it MAY recompute built-ins in a program that holds no clause of the program under check (Section 9.6). It establishes seven conditions and records each failure with its condition, a detail and, where there is one, the term concerned.
The document MUST read (Section 6.2); otherwise C3 fails and the document has
no claims and no steps. A rule or a directive fails C3 and is set aside. Each step/4 MUST have bindings that form a proper list of
'Name' = Value pairs with Name an atom, and uses that form a proper list;
otherwise C3 fails and the step is set aside. No two steps MAY have identical
goals: a second step for a goal fails C3 and is set aside. Every other fact
that is not clause/3 is a claim (Section 8.1).
Each clause(N, Head, Body) record MUST be the record of Section 8.2 for
program clause N, up to renumbering its minted variables in order of first
occurrence within the record.
For a rule(N) or fact(N) step, N MUST be a clause number of the program,
and for fact(N) the clause MUST be a fact. The clause, renamed apart, MUST
satisfy: each binding names a distinct variable of the clause and unifies it
with its value; the head unifies with Goal; and the body, of the same length
as Uses, unifies with Uses pairwise, such that afterwards the head is
identical to Goal and each body goal to its use. A step’s own terms MUST NOT
need further instantiation to match: a clause same(X, X) cannot justify
same(a, b), and a fact goal(_, y) justifies goal(x, y) only when the
document’s Goal is goal(x, y) itself.
No step MAY depend on itself through the conjuncts of the uses of steps.
By MUST be one of the forms of Section 8.3, other than unproven, which
always fails C3. A builtin step MUST have a callable goal. An absent step
MUST have a goal \+ G and a collected step a goal findall(T, G, L);
otherwise the justification is unknown. Neither MAY have bindings or uses.
Each conjunct of each claim MUST have a step. Each conjunct of each use MUST have a step or be an instance of a fact of the program. A document without claims is valid and certifies nothing.
A builtin step is re-decided: its goal is solved, for its first
solution, against a program that holds the bundled libraries the document’s
goals need (a goal qualified with a bundled library’s module loads that
library) and no clause of the program under check, so a goal only the
program could satisfy cannot succeed. The step agrees when the goal succeeds
and is afterwards a variant of itself, that is, solving it bound nothing but
fresh variables. It fails C5 when the goal fails, binds something, or raises
an error other than an existence error for a procedure. When the goal raises
an existence error, the predicate is not one the libraries define, and the
step cannot be re-decided.
A builtin step whose goal is one of the following is never re-decided: a
reflective goal, which reads the program’s own database or syntax
(clause/2, current_predicate/1, current_op/3), or a stateful goal,
which depends on attribute, constraint or stream state the run built up, or
would perform I/O (get_atts/2, put_atts/2, open/3,4, close/1,2,
read/2, read_term/3, write/2, write_term/3, nl/1, set_input/1,
set_output/1, current_input/1, current_output/1, at_end_of_stream/1,
stream_property/2, put_char/2, put_code/2, put_byte/2, get_char/2,
get_code/2, get_byte/2, peek_char/2, peek_code/2, peek_byte/2,
writeq/2, print/2, write_canonical/2, format/3, flush_output/1,
set_stream_position/2, gensym/2, reset_gensym/0,1, the CLP(B) sat/1,
taut/2, sat_count/2 and weighted_maximum/3, and the CLP(Z) fd_var/1,
fd_inf/2, fd_sup/2, fd_size/2, fd_dom/2 and fd_degree/2). Such a step, and one
that cannot be re-decided, is a trusted boundary of kind builtin, with the
reason reflective, stateful or theory_scoped.
A control step MUST have no bindings, and its uses MUST be identical, in
order, to one of the alternatives of its goal:
| Goal | Alternatives |
|---|---|
call(G), once(G), ignore(G), catch(G, C, R), M:G |
the conjuncts of G |
(C -> T), (C *-> T) |
the conjuncts of C, then those of T |
(C -> T ; E), (C *-> T ; E) |
the conjuncts of C, then those of T; or \+ C, then the conjuncts of E |
(A ; B) |
the conjuncts of A; or the conjuncts of B |
A builtin step with uses whose goal has alternatives and cannot be
re-decided is held to the same rule, as written by earlier versions.
An absent step whose goal is ground and whose inner goal is not one that
cannot be re-decided is re-decided as a builtin step is: when the re-decision
agrees, the step is checked rather than trusted, and when it disagrees, C5
fails. Otherwise absent, collected and asserted steps are trusted
boundaries of their own kind, with the reason theory_scoped. When trusted boundaries are forbidden
(“strict”), each trusted boundary, of any kind, fails C5.
A trusted absence or collection cannot be proved, but the evidence at hand can refute it.
A predicate is evidential when it has clauses in the program, is not
declared dynamic, is not the target of an assert/1, asserta/1,
assertz/1, retract/1, retractall/1 or abolish/1 call written with a
callable argument (or a Name/Arity indicator) in any program clause, is not
the key of an asserted step, and every goal of every one of its clause
bodies is, through , and ; but not -> or *->, either a call of an
evidential predicate or one of true/0, fail/0, false/0, =/2, is/2,
the arithmetic comparisons, member/2, append/3, select/3, between/3,
succ/2 and plus/3. When any program clause calls a database update with a
variable argument, no predicate is evidential. A recursive call is assumed
evidential while its predicate is being decided.
The evidence for a goal is:
,, ;, ->, *->, \+,
call/1, once/1, ignore/1, catch/3, :/2, findall/3,4, forall/2,
bagof/3, setof/3, aggregate_all/3,4), none: the boundary is left
undecided;Then:
\+ G is decided when G is a single goal, or a ground
conjunction, whose every conjunct has evidence. It fails C6 when every
conjunct of G unifies with some of its evidence.findall(T, G, L) fails C6 when L is not a proper list, and
is decided when G is a single goal with evidence. It fails C6 when, for
some evidence E of G, the instance of T under the unifier of G and
E unifies with no element of L.Evidential predicates are pure positive Horn clauses, so a call of one
finitely fails only when no instance of it is provable, and a completed
findall/3 over one has enumerated all of its provable instances. That is
what makes the evidence able to refute a boundary. A boundary that is not
refuted remains an obligation (Section 10).
The questions are the goals the proof answers (Section 4). When there
are none and the program has forward rules (Conclusion :+ Premise, run to a
fixed point when no goal is asked), the questions are, for each forward rule,
each conjunct of its conclusion other than false, and, for a rule whose
conclusion is true, its premise. Each claim
MUST be an instance of a question: unifying a fresh copy of the question with
the claim must leave the claim identical to itself. Each step MUST be
reachable from a conjunct of a claim through the conjuncts of uses.
| Condition | Covered |
|---|---|
| C1 resolution | rule and fact steps that passed C1 |
| C2 well_founded | steps |
| C3 justification | steps |
| C4 coverage | claims plus the uses of all steps |
| C5 re_decision | builtin and absent steps that agreed plus control steps that composed |
| C6 boundary_consistency | boundaries decided |
| C7 relevance | claims plus steps |
Steps set aside while reading (Section 9.1) are not counted. A check also
counts the steps, the claims, the steps verified by C1, the
builtin steps recomputed by C5, the steps composed by C5, and the
trusted boundaries.
A proof is valid when no condition failed. A valid proof with trusted boundaries is valid conditional on them.
A valid proof establishes that each of its claims follows from the program by the recorded steps, given its trusted boundaries. It does not establish that the claims are all the answers of the program, that the program terminates, or that the program is the one intended: a proof MAY leave answers out, and a run’s own proof holds exactly its claims.
A check report is a document holding, in this order, one fact per line:
condition(Id, Name, Outcome, Covered) for C1 to C7, where Name is the
name of Section 9.9, and Outcome is ok or failed(N), N the number
of that condition’s failures;failure(Condition, Subject, Detail) per failure, where Subject is the
term concerned or proof_document, and Detail an atom;obligation(Kind, Reason, Goal) per trusted boundary, in step order,
where Kind is builtin, absent, collected or asserted and Reason
is theory_scoped, reflective or stateful;steps(N), verified(N), recomputed(N), composed(N), trusted(N),
claims(N), the counts of Section 9.9;verdict(V), where V is failed(N) when N failures were recorded,
otherwise checked_with_obligations when there are trusted boundaries,
otherwise checked.Terms are written as in Section 6.1, with the variables of each fact renamed
A, B, …, Z, A1, …, Z1, A2, … in order of first occurrence.
A report is ordinary data: a program MAY load it as facts.
Failures are listed in the order they are found: those of reading the document (Section 9.1), in document order; C1 for each clause record, in record order; C3 for each duplicate step, in document order; C4 for each claim, in claim order; then for each step, in document order, C4 for its uses and the C1, C3 or C5 failure of its justification; C6 for each boundary, in step order; C7 for each claim, then for each step; and C2.
Detail is a short human-readable text that names what failed, often with
the written text of a term; it is informative, and implementations MAY word
it differently. EyeProlog’s details are, by condition:
| Condition | Details |
|---|---|
| C1 | clause record differs from source, unknown clause ..., clause N has a body, so it is not a fact, not an instance of source clause N: ... |
| C2 | cyclic derivation at ... |
| C3 | the document does not read: ..., a proof document holds facts only, step bindings must be a list of 'Name' = Value pairs and uses a list, duplicate justification for ..., invalid builtin justification, trusted boundaries cannot have bindings or uses, recorded as unproven, unknown justification ... |
| C4 | unjustified claim ..., unjustified use ... |
| C5 | primitive disagrees: ..., primitive went wrong: ..., control step does not follow from its uses: ..., trusted boundary forbidden: Kind |
| C6 | absence contradicted by evidence: ..., collected result is not a proper list: ..., collection misses ...: ... |
| C7 | claim answers no goal: ..., step serves no claim: ... |
The JSON form of a report is an object with valid (boolean), steps,
claims, verified, redecided (the count recomputed), composed,
uses (the number of uses of all steps, integers), trusted (a list of
{kind, reason, conclusion}), failures (a list of
{condition, detail, conclusion?}) and conditions (a list of
{id, name, covered, failed}), where conclusion is the written text of the
term concerned.
A proof can be read as one side of an argument. In the dialogue logic of Lorenzen and Lorenz, a proponent asserts a claim and an opponent may challenge every assertion that is not common ground; the proponent answers a challenge by naming what the assertion follows from, and the claim holds when the proponent can answer every challenge. A checked proof is a defence of this kind: the proponent’s answers are its steps, and the opponent is the checker (Section 9).
A dialogue is held for each answer of a run, in answer order, numbered from
claims(Claim). The steps of the run’s
proof (Section 8.3) are then visited from the claim, depth first and left to
right through the uses of each step, and each goal visited gives these moves:| Goal’s step | Moves |
|---|---|
rule(N) or control |
the opponent’s why(G), then the proponent’s because(G, By, Uses) |
fact(N), or no step (a use given by a fact) |
the opponent’s concedes(G) |
builtin or absent that the check re-decided |
the opponent’s verifies(G) |
builtin or absent the check trusted, collected, asserted |
the opponent’s grants(G) |
unproven |
the proponent’s gives_up(G) |
A goal already visited in the same dialogue gives only the opponent’s
concedes(G): it has been established. A failure the check recorded for a
step’s conclusion (Section 10) gives the opponent’s
objects(G, Condition, Detail) after the moves of that step, and ends the
dialogue, lost.
The opponent MAY hold evidence: clauses added to the program, which the
proponent did not use. Before it grants or verifies an absent step \+ G,
the opponent then solves G in the program with its evidence. When G has a
solution, the opponent’s move is counters(\+ G, Instance, Used), where
Instance is the first solution and Used the list of the evidence’s clauses
in the first proof of Instance, in the order that proof visits them; the
defence is lost.
A countered defence is followed by the proponent’s retracts(Claim, By), where
By is the justification of the claim’s step. Under the formal rule of
dialogue logic the proponent MAY then use what the opponent asserted: the run
is made again on the program with the evidence, and when the claim is among
its answers, its dialogue continues with the moves of that run’s proof, which
no evidence counters. Otherwise the proponent’s last move is
gives_up(Claim).
A dialogue document holds, for each dialogue in order, one fact per line:
move(Dialogue, N, Speaker, Act) for each move, N counting from 1 and
Speaker being proponent or opponent;outcome(Dialogue, Claim, Result), Result being won when no move lost
the defence and lost otherwise;obligation(Dialogue, Goal) for each grants(Goal) of a won dialogue’s
final defence, in move order: what the proponent’s win still rests on.Terms are written as in Section 6.1. A dialogue document is ordinary data: a program MAY load it as facts.
eyeprolog [OPTION ...] [FILE-OR-URL ... | -]
The options that concern this document are:
| Option | Meaning |
|---|---|
| (none) | Load the sources, or standard input, as one program and print its answers (Section 5). |
-p, --proof |
Print the proof document (Section 8) instead. |
--proof-detail abstract\|expanded |
Select the proof detail (Section 7); implies --proof. |
-g, --goal GOAL |
Ask GOAL; MAY be repeated (Section 4). With --check-proof, the goals the proof answers. |
--check-proof FILE |
Check the proof in FILE (- for standard input) against the program and print its report (Section 10). |
--strict-proof |
With --check-proof, forbid trusted boundaries. |
--json |
With --check-proof, print the report as JSON. |
--quiet |
With --check-proof, print only the verdict/1 fact. |
-d, --dialogue |
Print the dialogue document (Section 11) instead of the answers. |
--evidence FILE |
Give the opponent the clauses of FILE as evidence (Section 11.2); implies --dialogue. |
--iso-strict, --no-autoload |
Select the language profile (Section 3). |
-h, --help, -v, --version |
Print the usage, or the version. |
--dialogue MUST NOT be combined with --check-proof, --quads or
--iso-strict. --check-proof MUST NOT be combined with --proof or --quads, and --json
and --strict-proof need --check-proof. With --check-proof - the proof is
read from standard input, so the program MUST be named as a file:
eyeprolog --proof p.pl | eyeprolog --check-proof - p.pl
A program text with a line starting with step(, no line starting with :-
and no declared goal is a proof document; given one as a program without
goals, the command line MUST say how to check it instead.
| Exit code | Meaning |
|---|---|
| 0 | Success, including a check that found the proof valid. |
| 1 | An error, printed to standard error as eyeprolog: message, including a run whose proof does not check (Section 7.1). |
| 2 | A check that found the proof not valid; the report is printed as usual. |
A program MAY choose its own exit status with halt/1.
A program is Prolog code and runs with the privileges of whoever runs it; it MAY read and write files, open sockets and run initialization goals. Only programs from trusted sources should be run.
A document (answers, proofs and check reports) is untrusted data. It MUST NOT be executed: it is read as clauses (Section 6.2), so no directive in it runs, and the checker consults it only by unification and comparison. Checking a proof from a third party therefore runs none of the third party’s code. C5 runs built-in goals the document records, but in a program that holds only the bundled libraries, and never a stream operation (Section 9.6); a deployment that checks untrusted proofs SHOULD still bound document size, nesting depth and running time, since a recorded goal MAY be expensive to recompute.
A valid proof establishes that its claims follow from the program supplied to the checker (Section 9.10). It does not establish that the program is correct or that the claims are all its answers, and a proof with obligations holds only conditional on them.
A conforming reasoner implements Sections 3 to 8, produces answers and
proof documents in the written form of Section 6, and checks every proof it
produces as Section 7.1 requires. A conforming checker
implements Sections 8 to 10 and does not depend on a reasoner. For the same
program and goals, a conforming reasoner and checker MUST produce the same
answers, proof documents, reports and dialogue documents as eyeprolog 1.6.42, byte for byte,
except for the Detail texts of failures (Section 10) and where the host’s
floating-point library functions differ in the last digit.
The repository’s examples, with their saved answers (examples/output/),
proofs (examples/proof/) and reports (examples/check/), test this on 239
programs, each with its proof; npm test regenerates and re-checks every one of them, as well as
the proof cases of the conformance suite in test/conformance/proofs/.
A document is Prolog text read with the operators and flags of the program it
belongs to (Section 6.2). Its clauses are facts of these forms, in the ABNF
style of RFC 5234, where term is an ISO Prolog term at priority 999 and
claim any other callable term:
proof = *( claim "." ) [ blank *( record "." ) ] [ blank *( step "." ) ]
record = "clause(" integer "," template "," template ")"
template = term ; variables written as var('X') or anonymous(I)
step = "step(" term "," by "," bindings "," uses ")"
by = "rule(" integer ")" / "fact(" integer ")" / "builtin" / "control"
/ "absent" / "collected" / "asserted" / "unproven"
bindings = "[" [ binding *( "," binding ) ] "]"
binding = quoted-atom "=" term
uses = "[" [ term *( "," term ) ] "]"
report = 7condition *failure *obligation counts verdict
condition = "condition('" id "', " name ", " outcome ", " integer ")."
id = "C1" / "C2" / "C3" / "C4" / "C5" / "C6" / "C7"
name = "resolution" / "well_founded" / "justification" / "coverage"
/ "re_decision" / "boundary_consistency" / "relevance"
outcome = "ok" / "failed(" integer ")"
failure = "failure('" id "', " term ", " quoted-atom ")."
obligation = "obligation(" kind ", " reason ", " term ")."
kind = "builtin" / "absent" / "collected" / "asserted"
reason = "theory_scoped" / "reflective" / "stateful"
counts = "steps(" integer ")." "verified(" integer ")." "recomputed(" integer ")."
"composed(" integer ")." "trusted(" integer ")." "claims(" integer ")."
verdict = "verdict(" ( "checked" / "checked_with_obligations"
/ "failed(" integer ")" ) ")."
Line breaks and layout inside a term are free; the documents EyeProlog writes put each claim and report fact on one line and MAY break a long clause record or step across several.
The program socrates.pl:
%% ?- mortal(X).
human(socrates).
human(plato).
god(zeus).
mortal(X) :- human(X), \+ god(X).
Its answers:
mortal(socrates).
mortal(plato).
Its proof document (Section 8):
mortal(socrates).
mortal(plato).
clause(1, human(socrates), true).
clause(2, human(plato), true).
clause(4, mortal(var('X')), (human(var('X')), \+ god(var('X')))).
step(mortal(socrates), rule(4), ['X' = socrates], [human(socrates), \+ god(socrates)]).
step(human(socrates), fact(1), [], []).
step(\+ god(socrates), absent, [], []).
step(mortal(plato), rule(4), ['X' = plato], [human(plato), \+ god(plato)]).
step(human(plato), fact(2), [], []).
step(\+ god(plato), absent, [], []).
Its check report (Section 10). Both absences are decided by C6, since god/1
is evidential and no fact or step shows god(socrates) or god(plato), but a
decided boundary that is not refuted is still an obligation:
condition('C1', resolution, ok, 4).
condition('C2', well_founded, ok, 6).
condition('C3', justification, ok, 6).
condition('C4', coverage, ok, 6).
condition('C5', re_decision, ok, 0).
condition('C6', boundary_consistency, ok, 2).
condition('C7', relevance, ok, 8).
obligation(absent, theory_scoped, \+ god(socrates)).
obligation(absent, theory_scoped, \+ god(plato)).
steps(6).
verified(4).
recomputed(0).
composed(0).
trusted(2).
claims(2).
verdict(checked_with_obligations).
Had the document claimed mortal(zeus) with the step
step(\+ god(zeus), absent, [], []), C6 would have failed it: the fact
god(zeus) is evidence that the absence did not hold.
This appendix is informative: it describes how this version of EyeProlog implements this document, not requirements on other implementations.
| File | Responsibility |
|---|---|
| src/execute.js | Solving goals and reporting answers (Section 5) |
| src/goal-metadata.js | Declared %% ?- goals (Section 4) |
| src/explain.js | The proof replay, clause numbering and the flat proof (Sections 3, 7, 8) |
| src/result-format.js | Writing answers, clause records and steps (Sections 6, 8) |
| src/proof-document.js | Checking a run’s own proof before it is written (Section 7.1) |
| src/check-proof.js | Reading and checking proof documents and writing reports, with no search of the program (Sections 9, 10) |
| src/dialogue.js | Playing a checked proof out as a dialogue (Section 11) |
| src/cli.js | The command line (Section 12) |
| test/run-proof-checking.mjs | Re-checking every packaged proof against its saved report |
The proof is a replay, not a trace. The engine answers goals without recording anything; when a proof is asked for, each answer is replayed against the program until its first derivation is found. The replay resolves every node of that derivation again once it is complete, so a goal solved early in a derivation is recorded with the bindings later goals gave it.
Deep derivations are replayed iteratively. A ground goal that a chain of single-goal clauses proves, each with exactly one matching clause, is followed directly, so a taxonomy thousands of levels deep is proved without a host call frame per level. Past its nesting budget the general replay continues as a chain (Section 7), flattening its binding history as it goes, and the derivation is resolved once at the end with every variable chain remembered, so a recursion threading an output argument through ten thousand levels is explained in time linear in its depth.
A reasoner checks its own proofs in memory. The proof a run builds is
checked as the claims, clause records and steps it is written from, which
gives the report reading the written document back would give, without
writing and reading it; --check-proof reads and checks the text. That the
two agree is what checking the packaged documents establishes.
C5 is independent by construction. The program a builtin step is
re-decided in is built once per document, from an empty source with the
libraries the recorded goals autoload. No clause of the program under check
is present, so the re-decision cannot be talked into agreeing by the rules it
audits.
C6 asks only evidence it can trust. Prolog’s cuts, if-then-else, type tests and negation make a call with fewer bindings able to answer differently from one with more, so evidence about one call says nothing about another. The checker therefore takes evidence only from predicates whose definitions are static and pure positive Horn clauses all the way down (Section 9.7), and leaves every other boundary undecided rather than guessing.
A check is ordinary Prolog. The report is written by the same writer as
the answers and proofs, with the program’s operators, so \+ G in an
obligation reads exactly as it did in the proof.