eyedia
Examples
Eyedia — reasoning you can see.
Every example also has a card deck that explains it for a wide audience.
Run a source, generate its proof, or check its saved proof:
node bin/eyedia.js examples/socrates.pl
node bin/eyedia.js --proof examples/socrates.pl
node bin/eyedia.js --check-proof examples/proof/socrates.pl examples/socrates.pl
Each program has a matching conclusion file in output/, a certificate in
proof/, and a Prolog C1-C7 verification report in check/. The names match the
source: lists.pl has output/lists.pl, proof/lists.pl and check/lists.pl.
| Program | Demonstrates |
|---|---|
| socrates.pl | Class membership derived through a subclass rule |
| deep-taxonomy-10.pl | A ten-level subclass chain with branches that lead nowhere |
| deep-taxonomy-100.pl | The same taxonomy benchmark at a hundred levels |
| deep-taxonomy-1000.pl | The same taxonomy benchmark at a thousand levels |
| deep-taxonomy-10000.pl | The same taxonomy benchmark at ten thousand levels |
| backward.pl | Backward definitions inside forward bodies |
| fibonacci.pl | Fast doubling for exact Fibonacci numbers, and the golden ratio |
| graphs.pl | Base data, negation and collection |
| terms.pl | Quoted graphs, triple terms and residual witnesses |
| reachability.pl | Finite closure in a graph containing a cycle |
| shortest-path.pl | Weighted paths and stratified minimum selection |
| path-discovery.pl | Full airport network with configurable endpoints and maximum stopovers |
| lists.pl | Concatenation, mapping and summation |
| strings.pl | Text construction and Unicode inspection |
| inventory.pl | An invoice from collected line totals |
| dog-license.pl | A licensing threshold based on collected dog counts |
| permissions.pl | Role permissions with exclusions |
| witnesses.pl | Structured witnesses and shared multi-head conclusions |
| state-transitions.pl | Account balances from an ordered event log |
| integrity.pl | A provable integrity violation |
| alternatives.pl | Alternative routes, disjunction and once |
| unification.pl | Open lists and repeated-variable constraints |
| schema-inference.pl | Subclasses, subproperties, domains and ranges |
| family-cousins.pl | Generations, family branches and cousin relationships |
| hanoi.pl | Recursive construction of a disk-move sequence |
| collatz.pl | Parity-based recursive trajectories over a range of starts |
| flat-map.pl | Predicate-based mapping with multiple or missing values |
| paraconsistent-animals.pl | Local summaries of conflicting observations |
| scoped-audit.pl | Presence and absence within separate quoted graphs |
| control-system.pl | Feedforward and nonlinear feedback commands for two actuators |
| lldm.pl | Leg length discrepancy measured from radiograph landmarks, with an alarm and its reason |
| variable-predicates.pl | Relations selected and renamed through data bindings |
| good-cobbler.pl | Trade-specific classification from structured descriptions |
| peano.pl | Symbolic arithmetic, relational addition and a chained derivation |
| expression-eval.pl | Recursive expression graphs used in forward inference |
| complex.pl | Complex arithmetic, exact over Gaussian integers and polar beyond them |
| polynomial.pl | Complex roots of polynomials up to degree 4 by Cardan and Lagrange |
| interval-relations.pl | All thirteen interval relations and endpoint completion |
| bayes-diagnosis.pl | Normalized probabilities for illustrative printer faults |
| policy-risk.pl | Ranked findings with explanations and suggested mitigations |
| research-portal.pl | A hospital research portal combines ODRL/DPV policy decisions with Digital Omnibus device consent and breach plans |
| package-holiday.pl | Package holiday cancellations under the tour operator’s ODRL terms and the 2015 and revised EU Package Travel Directive |
| queens.pl | Configurable N-queens search with diagonal constraints |
| age.pl | Calendar-year and elapsed-day age checks at an explicit reference date |
| ackermann.pl | The Ackermann function through the hyperoperation sequence, exactly |
| peasant.pl | Peasant multiplication and exponentiation by halving and doubling |
| sieve.pl | The sieve of Eratosthenes over an explicit list of integers |
| goldbach.pl | Goldbach splits of every power of two up to 2^25 |
| kaprekar.pl | Every four-digit Kaprekar routine reaches 6174 within seven steps |
| easter.pl | Easter Sunday by the anonymous Gregorian algorithm, 2021 to 2050 |
| turing.pl | A Turing machine interpreter running a binary incrementer |
| zebra.pl | The zebra puzzle solved by narrowing five partially known houses |
| aunt-agatha.pl | Who killed Aunt Agatha? A conclusion entailed by holding in every model of the premises |
| four-color.pl | Four-colouring the map of the European Union |
| wolf-goat-cabbage.pl | The river crossing, with seven crossings shown to be minimal |
| monkey-bananas.pl | Every plan of up to five moves that gets the monkey the bananas |
| gps.pl | Goal-driven parallel sequences: routes to a goal state within duration, cost, belief and comfort limits |
| superdense-coding.pl | Superdense coding in discrete quantum theory, with interference as odd path counts |
| teleportation.pl | Quantum teleportation in discrete quantum theory, checked for every state and outcome |
integrity.pl intentionally exits with code 65 because it concludes false.
Its proof-check report is valid: the certificate explains why the constraint was
violated. Negation and collection examples list their absent and collected
obligations in the check report; --strict-proof rejects those obligations.
Every check file includes condition/4 facts for C1-C7, verification counts and
a verdict/1 fact. Reports with failures include failure/3; reports with
trusted boundaries include obligation/3. Add --json to the check command
for JSON output instead of Prolog facts.
fibonacci.pl answers F(0), F(1), F(10), F(100), F(1000) and F(10000), the
last a 2090-digit integer, then divides successive values to watch the ratio
converge on the golden ratio. It uses fast doubling, which halves the index at
each recursive step and fits within the default reasoning limits. Its saved
proof records the arithmetic and recursive clause instances without trusted
obligations.
The deep-taxonomy examples are the deep-taxonomy benchmark: one individual, a
chain of subclass rules, and two sibling branches at every level that lead
nowhere. The goal has to follow the single productive branch the whole way
down, so the chain length is also the backward recursion depth. The four sizes
run from ten to ten thousand levels, and each costs exactly one resolution
step per level, which --stats reports and the saved check report confirms:
deep-taxonomy-10000 verifies 10001 steps. Backward search is an explicit
machine, so the depth costs heap rather than host stack.
node bin/eyedia.js --stats examples/deep-taxonomy-10000.pl
Time, proof size and checking all grow linearly with the depth, so a longer chain only costs proportionally more; the ten-thousand-level source is about 1 MB and its certificate about 1.3 MB, since a certificate records every step it claims.
path-discovery.pl contains 7,698 airport records and 37,505 directed
connections. Its default goal finds three routes from Ostend to Prague with
at most two stopovers. Use any airport-name atoms and a nonnegative integer
limit with path_discovery(From, To, MaxStopovers, Path):
node bin/eyedia.js --goal "path_discovery('Liège Airport', 'Václav Havel Airport Prague', 1, Path)" examples/path-discovery.pl
goal="path_discovery('Ostend-Bruges International Airport', 'Liège Airport', 0, Path)"
node bin/eyedia.js --proof --goal "$goal" examples/path-discovery.pl > /tmp/route-proof.pl
node bin/eyedia.js --strict-proof --check-proof /tmp/route-proof.pl --goal "$goal" examples/path-discovery.pl
--goal replaces the default goal, so checking that proof names the same goal. Zero stopovers allows only direct flights;
N stopovers allows at most N+1 flights. Routes follow the recorded direction
and never repeat an airport. Equal endpoints and unknown names return no
routes. Negative or noninteger limits also return no routes. You can leave
From or To as a variable to discover endpoints; keep MaxStopovers bound.
List the available names with --goal "airport(Id, Name)". These are historical
network records, rather than current flight schedules. The search uses explicit
disequalities to prevent cycles, so its proofs have no trusted obligations.
Large bounds on a dense network may still reach the configured reasoning limits.
peano.pl represents natural numbers as zero, s(zero), and so on. Its
addition goal enumerates every split of a known sum, and a second goal chains
all three relations: (1*2)+3 is 5, whose factorial is 120 nested successors.
expression-eval.pl evaluates a graph for (2*3)+(10-4) and emits
result(example, 12).
complex.pl adds a numeric domain the engine knows nothing about. A complex
number is the ordinary term complex(Real, Imaginary), and addition,
multiplication, conjugation, division, norm, modulus and integer powers are all
ordinary clauses over integer arithmetic. Components stay exact wherever the
arithmetic allows it: dividing complex(-5, 10) by complex(1, 2) recovers
complex(3, 4) as integers because the norm divides both parts, while the same
division applied to complex(3, 4) yields the float pair complex(2.2, -0.4).
The example also derives i*i = -1 from the multiplication clause rather than
assuming it, confirms that the Gaussian norm is multiplicative, and raises
complex(1, 1) to the eighth power by repeated squaring.
Polar form then leaves the integers altogether, so a complex number can be
raised to a complex power. The square root of -1 is i, e to the power i*pi
is -1, i to the power i is the real number 0.20787957635076193, and the
inverse sine and cosine of 2 are complex. Logarithm, sine, cosine, tangent and
arctangent follow, each applied to the answer of its own inverse so the
round trip is visible: the sine of the arcsine of 2 comes back as 2. The example
passes strict proof checking, so every component of every conclusion is
recomputed by the checker:
node bin/eyedia.js --goal "complex_power(complex(1, 1), 16, Result)" examples/complex.pl
node bin/eyedia.js --goal "complex_div(complex(1, 0), complex(0, 1), Inverse)" examples/complex.pl
polynomial.pl is Alain Colmerauer’s solver for polynomial equations up to
degree 4, with complex coefficients and roots as [Re, Im] pairs. Degree 3
follows Cardan’s formula and degree 4 Lagrange’s method, which solves a cubic
on the way. Its default goals find the roots of (x-1)(x-2)(x-3)(x-4) and of a
quartic with complex coefficients whose roots are 3+2i, 5+i, i and 1+i, each
up to rounding. The original evaluates expressions by building calls with
=..; here each operation has its own clause, and the zero tests compare
numbers instead of cutting. Lagrange’s step collects the roots of a cubic with
a predicate of its own, so that collection depends only on a lower degree.
A list of all roots is a completed collection, so the default certificate is
small: four steps, with the arithmetic inside two collected obligations. Ask
for one root at a time and every arithmetic step is in the certificate
instead. For a cubic it passes strict checking:
node bin/eyedia.js --proof --goal "racine([[1, 0], [-6, 0], [11, 0], [-6, 0]], Z)" examples/polynomial.pl
queens.pl returns the first solution for an 8x8 board by default; another
goal enumerates other board sizes:
node bin/eyedia.js --goal "queens(4, Columns)" examples/queens.pl
node bin/eyedia.js --goal "add(A, B, s(s(s(zero))))" examples/peano.pl
interval-relations.pl uses half-open intervals with integer-minute endpoints.
It completes endpoints from durations and classifies each valid interval pair
into exactly one of thirteen relations. Empty and reversed intervals are
excluded from classification.
control-system.pl computes two actuator commands. The first is a
proportional part on a conditioned measurement minus a feedforward
compensation, the base-10 logarithm of a measured disturbance. The second is
a proportional, nonlinear differential feedback controller on the error
between a target and an output. The results are ordinary floats, and the proof
recomputes every arithmetic step.
lldm.pl measures a leg length discrepancy from four landmarks on a
radiograph. Two landmarks fix a reference line, and each leg runs from one of
the other two to its perpendicular projection on that line. With a 1.25 cm
threshold the measured legs, 21.55 cm and 23.46 cm, raise an alarm, printed
with the lengths, the discrepancy, the threshold and the reason. The reason
names the side of the threshold that fired; the version this was adapted from
gave the same reason for both. Every intermediate value is a separate val/3
clause, so the strict certificate recomputes each one.
bayes-diagnosis.pl models printer faults using illustrative priors and two
conditionally independent observations. It keeps exact integer likelihood
weights and their collected total alongside a floating-point probability.
policy-risk.pl reports a rank, clause, clamped score, severity, reason and
mitigation. Rank 1 has the highest score; equal scores share a rank. Output
follows inference order, with ranks recorded explicitly. Adding the missing
safeguards removes the affected findings. Both examples expose their collection
obligations, and policy findings also expose absence obligations.
research-portal.pl evaluates a hospital research portal under two rulebooks.
An ODRL/DPV policy decides research access first, then the baseline or
original Digital Omnibus rulebook decides the device-consent step. Eleven
sessions produce permits with planned deletion duties, pending device consent,
or explicit policy and device refusals. Three incidents have notification
plans under both regimes, always retaining internal documentation. Changes
compare final plans; a device exemption never overrides withdrawn research
consent or a prohibition.
package-holiday.pl is the same pattern in the domain of leisure. A tour
operator’s cancellation terms, written as an ODRL offer, decide first who may
cancel and at what fee; then the EU Package Travel Directive, in its 2015
version and as revised in 2026, decides when a cancellation is free and how
the money comes back. Eight cancellations and two complaints are decided
under both versions, with fees and refunds computed in euro. The revision
makes a cancellation free when floods close the departure airport, gives
accepted vouchers statutory guarantees, and sets complaint deadlines. Every
condition of the terms is checked one by one, so the proof passes
--strict-proof with no trusted steps.
age.pl checks whether a person’s age strictly exceeds years(N) or days(N).
It uses as_of(date(2026, 10, 1)) for reproducible output and proofs. Edit that
fact to change the default date, or pass a reference date directly:
node bin/eyedia.js examples/age.pl
node bin/eyedia.js --goal "age_above(pat_h, years(80), date(2024, 8, 22))" examples/age.pl
node bin/eyedia.js --goal "age_days(pat_h, date(2026, 10, 1), Days)" examples/age.pl
Exactly on the threshold anniversary, age_above/3 fails; it succeeds on the
following day. A February 29 anniversary falls on February 28 in a non-leap
year. Elapsed days follow the Gregorian calendar, including century leap-year
rules. Invalid dates, future births, unknown people, and negative or noninteger
thresholds return no answers. Reference dates are explicit source data rather
than clock readings, and the example passes strict proof checking.
The classics from ackermann.pl to teleportation.pl are written without a
library. Relations such as between/3, member/2 or length/2 are defined in
each program as ordinary clauses, and a search commits with once/1, or with
guards that make its alternatives exclusive, where Prolog would use cut.
ackermann.pl computes A(4, 2), a number with 19,729 digits, through the
hyperoperation sequence: addition, multiplication and exponentiation have closed
forms, and every higher level is the one below it iterated. peasant.pl
multiplies and raises to powers using only halving, doubling and addition.
sieve.pl lists the primes below 100 by striking out multiples from an
explicit list; it stops there because its certificate records every
intermediate list, which grows far faster than the answer.
goldbach.pl splits every power of two from 4 to 2^25 into two primes, taking
the split with the smallest prime. easter.pl dates Easter Sunday for 2021 to
2050 with the anonymous Gregorian algorithm, every step integer arithmetic on
the year. turing.pl is a Turing machine interpreter running a machine that
adds one to a binary number.
zebra.pl solves Einstein’s riddle by narrowing a list of five partially known
houses with unification alone. aunt-agatha.pl is Pelletier’s problem 55
(TPTP PUZ001), a classic test for theorem provers: nine premises about the
three residents of Dreadbury Mansion, and the claim that Agatha killed
herself. A puzzle like the zebra asks for one solution; this one asks what
follows, which is what holds in every situation the premises allow. The
premises leave open who hates whom and who is richer than whom, so the program
enumerates every model of them: Agatha is the killer in four, the butler and
Charles in none. A full model is printed as a witness, with a proof that each
premise holds in it. four-color.pl colours the 27 countries of the
European Union so that no neighbours share a colour. wolf-goat-cabbage.pl
shows that a safe crossing takes seven trips and that no shorter one exists,
then prints both seven-trip plans. monkey-bananas.pl lists every plan of up
to five moves that gets the monkey the bananas, shortest first.
gps.pl is goal-driven parallel sequences: it finds sequences of actions from
the current state to a goal state, here driving from Gent to Oostende on a
partial map of Belgium. Duration and cost add up along a path and belief and
comfort multiply, and each must stay within its limit, as must the number of
stages, runs of steps in the same map. Two routes qualify, directly through
Brugge and the longer one through Kortrijk. The original keeps the current
state in the database, reading transitions with clause/2 and asserting and
retracting fluents as it moves; here the state is a list of fluents passed
along the search, so every step is an ordinary clause instance and the
certificate passes strict checking. Stages are counted as changes of map plus
one, where the original stops counting at two.
superdense-coding.pl sends two classical bits through one qubit in discrete
quantum theory, where amplitudes come from a finite field and the merge of
alternative branches is exclusive: an answer survives when it is reached an odd
number of times. The original toggles asserted facts to get that parity; here
each of Alice’s messages N and Bob’s readings M collects its ways through the
shared entangled pair and keeps the pair when their number is odd. Every
message arrives as itself by exactly one way, and every wrong reading by two
ways that cancel or by none, so Bob reads 0 to 3 exactly as Alice sent them.
The parity depends on all the ways, so the certificate carries the four
collections behind its answers as obligations.
teleportation.pl runs the companion protocol in the same theory, with the
same relations. Alice measures the qubit to send together with her half of the
entangled pair, in the four-state basis Bob decodes with in superdense coding,
and sends him the outcome. Bob applies the inverse of that basis relation, which
turns out to be one of Alice’s four operations from superdense coding, to his
half. For each of the three nonzero states over the two-element field and each
of the four outcomes, Bob ends up holding exactly the state Alice sent, and a
false :+ rule would stop the run with exit code 65 if he did not. The
protocol was written for this collection, not taken from a sibling project.
Certificates that lean on a completed search say so. In kaprekar.pl the whole
verification sits inside one negation, so its certificate is two steps plus an
absent obligation: the exhaustive check over 705 digit multisets is exactly
what the obligation names. four-color.pl collects the countries with
findall/3 and rules out conflicts with negation, so it carries both kinds.
Run npm test for the full suite or npm run test:examples for this corpus.
Every example runs through the API and all three CLI modes. The test log prints
[current/total] and the name of each test before executing it. Tests compare
results with saved artifacts and do not overwrite them.
After an intentional behavior change, run npm run examples:update and review
the source and artifact changes together. When adding an example, register its
name, description, expected halt code (if any) and proof obligations in
manifest.json, then generate its artifacts.