Examples

Each example comes with a short card deck that explains it for a wide audience: the question it asks, what the program says, what eyekind concludes, why, and what the proof checker confirms. Cards are separated by ---, so a deck reads as plain Markdown here and works as slides in Markdown slide tools such as Marp.

For practical decisions, try outage recovery, project scheduling, battery dispatch, cold-chain evidence, or school placement audits. For mathematical calculations, try Bézout certificates, Pell equations, binomial identities, least-squares regression, or Hamming codes.

Run a source, generate its proof, or check its saved proof:

python -m eyekind examples/socrates.py
python -m eyekind -c examples/socrates.py
python -m eyekind --proof examples/socrates.py
python -m eyekind --check-proof examples/proof/socrates.py examples/socrates.py

Each program has a matching conclusion file in output/, a certificate in proof/, and a C1-C8 verification report in check/, each written as Python expressions, one per line. The names match the source: lists.py has output/lists.py, proof/lists.py and check/lists.py.

The derived forward rule, derived backward rule, and conjunction of backward templates show rules enabled by other rules. Inline implies(Body, Head) and implied_by(Head, Body) templates capture their generating context and keep their other variables local. Arrays can join templates or the goals within one template. Each generated rule has a proved activation; its dependencies are visible to stratification before reasoning starts.

audited-grants.py shows what one language makes possible. It states an energy grant policy as a program of its own, has eyekind prove the decisions, and then reads that proof and its check report back as ordinary facts, with eyekind.read_terms and facts_from, to audit the reasoning: the data each decision rests on, the assumptions it took on trust, and the decisions at risk because they rest on self-declared income. Rules, data, conclusions, proof and report are all the same terms, so the audit needs no export format, no parser and no second tool, and its own conclusions come with a checked proof too.

integrity.py 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(...) facts for C1-C8, verification counts and a verdict(...) fact. Reports with failures include failure(...); reports with trusted boundaries include obligation(...). Add --json to the check command for JSON output instead.

fibonacci.py 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 five sizes run from ten to a hundred thousand levels, and each costs exactly one resolution step per level, which --stats reports and the saved check report confirms: deep-taxonomy-100000 verifies 100001 steps. Each program states its rules with a Python loop rather than one by one, which keeps even the largest a few lines long instead of 14 MB. Backward search is an explicit machine, so the depth costs heap rather than host stack.

python -m eyekind --stats examples/deep-taxonomy-10000.py

Time, proof size and checking all grow linearly with the depth, so a longer chain only costs proportionally more; the ten-thousand-level certificate is about 1.4 MB, since a certificate records every step it claims.

path-discovery.py 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):

python -m eyekind --goal "path_discovery('Liège Airport', 'Václav Havel Airport Prague', 1, Path)" examples/path-discovery.py
goal="path_discovery('Ostend-Bruges International Airport', 'Liège Airport', 0, Path)"
python -m eyekind --proof --goal "$goal" examples/path-discovery.py > /tmp/route-proof.py
python -m eyekind --strict-proof --check-proof /tmp/route-proof.py --goal "$goal" examples/path-discovery.py

--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.py 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.py evaluates a graph for (2*3)+(10-4) and emits result('example', 12).

complex.py 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. Sums, products, conjugates, norms and integer powers stay exact integers. Division uses div, which is true division: dividing complex(-5, 10) by complex(1, 2) recovers complex(3.0, 4.0), and the same division applied to complex(3, 4) yields 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:

python -m eyekind --goal "complex_power(complex(1, 1), 16, Result)" examples/complex.py
python -m eyekind --goal "complex_div(complex(1, 0), complex(0, 1), Inverse)" examples/complex.py

polynomial.py 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 univ); 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:

python -m eyekind --proof --goal "racine([[1, 0], [-6, 0], [11, 0], [-6, 0]], Z)" examples/polynomial.py

queens.py returns the first solution for an 8x8 board by default; another goal enumerates other board sizes:

python -m eyekind --goal "queens(4, Columns)" examples/queens.py
python -m eyekind --goal "add(A, B, s(s(s('zero'))))" examples/peano.py

interval-relations.py 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.py 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. Guards keep every input from stopping the run: the logarithm is taken only of a positive disturbance, and the nonlinear factor, which divides by the error, is left out when the output is on target.

lldm.py 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.py 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.py 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.py 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.py 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.

delfour.py shares a conclusion instead of the data behind it, in the scenario of Ruben Verborgh’s Inside the insight economy. A shopper’s phone turns a household’s diabetes into a neutral low-sugar insight, restricted to the Delfour supermarket and its self-scanner, expiring in two hours, wrapped with an ODRL policy and signed; the post leaves those details open, and the example fills them in. The scanner reasons only from that insight: it shows the sugar per serving of each product scanned, flags the 12 g biscuits against the 10 g threshold, and suggests the 3 g biscuits in aisle 7. Ten checks pass, among them that the shared text names no condition, found by searching it with atom_concat. That no other biscuit has less sugar and that the text holds neither “diabetes” nor “medical” are absences, listed as obligations. The signature is accepted because the input says it was verified upstream; the rules do not recompute the HMAC.

deontic-logic.py states duties as plain relations: alice was obliged to obtain consent and prohibited from sharing a record. Observations say what she did and, explicitly, what she did not do; a missed obligation is read only from an explicit not_performed fact, never from a missing observation. Notifying the data protection officer compensates the sharing, but the violation stays on record. Nothing compensates the missed consent, so alice’s status is requires_review, and the proof needs no trusted obligations.

nixon-diamond.py sets two defaults against each other: Quakers are pacifists and Republicans are nonpacifists, and nixon is both. The pacifist default is guarded by not_(nonpacifist(Person)), so the Republican rule takes priority, and stratification runs the default only after the nonpacifist rule has finished. nixon is classified as a nonpacifist and not as a pacifist, while ada, only a Quaker, gets the default. The proof rests on one absent obligation: that nothing concludes ada is a nonpacifist.

owl-property-chain.py defines grandparent as a chain of two parent links, stored as a plain list of property names next to the triples. One forward rule takes a chain’s first property and hands the rest of the list to a backward rule, follow_chain, which takes one link per property; the list gets shorter at each step, so the walk always ends. The program concludes that Alice is Carol’s grandparent and Bob is Dave’s. Declaring a longer chain needs no new rule.

age.py 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:

python -m eyekind examples/age.py
python -m eyekind --goal "age_above('pat_h', years(80), date(2024, 8, 22))" examples/age.py
python -m eyekind --goal "age_days('pat_h', date(2026, 10, 1), Days)" examples/age.py

Exactly on the threshold anniversary, age_above 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.py to teleportation.py are written without a library. Relations such as between, member or length are defined in each program as ordinary clauses, and a search commits with once, or with guards that make its alternatives exclusive.

ackermann.py 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.py multiplies and raises to powers using only halving, doubling and addition. sieve.py 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.py splits every power of two from 4 to 2^25 into two primes, taking the split with the smallest prime. easter.py dates Easter Sunday for 2021 to 2050 with the anonymous Gregorian algorithm, every step integer arithmetic on the year. turing.py is a Turing machine interpreter running a machine that adds one to a binary number.

zebra.py solves Einstein’s riddle by narrowing a list of five partially known houses with unification alone. aunt-agatha.py 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.py colours the 27 countries of the European Union so that no neighbours share a colour. wolf-goat-cabbage.py shows that a safe crossing takes seven trips and that no shorter one exists, then prints both seven-trip plans. monkey-bananas.py lists every plan of up to five moves that gets the monkey the bananas, shortest first.

gps.py 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.py 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.py 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 contradiction(...) 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.py 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.py collects the countries with findall and rules out conflicts with negation, so it carries both kinds.

Run ./test for the full suite, or ./test examples for this corpus; ./test -k socrates limits it to the tests that mention socrates. Every example runs through the API, and a few through all three CLI modes. Tests compare results with saved artifacts and do not overwrite them.

dijkstra.py finds a shortest route with Dijkstra’s algorithm on six places joined by nine two-way roads. It keeps a queue of partial routes sorted by cost, always extends the cheapest one, and settles each place the first time it leaves the queue. The route from a to f is a, c, b, d, e, f with length 13, the way back is the same route reversed, and a to a costs 0; a road list with a negative length is rejected. The cases of the search exclude each other through not_unify and a list walk instead of not_(...), so the proof takes nothing on trust.

knapsack-optimization.py chooses an expedition pack worth the most within a weight limit of 15 from eight items, each taken once or left out. A backward rule lists all 256 subsets and a forward rule keeps the 113 that fit; findall gathers their values into one list, whose length is the number of packs that fit and whose maximum, 40, is the best value. The only pack worth 40 takes the atlas, battery, camera, medkit and sensor, weighing exactly 15. The proof recomputes every sum and comparison and trusts one thing: that the collected list of values is complete.

type-inference.py works out the types of six small programs written as syntax trees: functions with typed parameters, calls, integer addition, conditionals and pairs. Each kind of expression has one backward typing rule, and an environment of [Name, Type] pairs, innermost first, handles parameter lookup and shadowing. A call is well typed when a shared variable makes the function’s parameter type and the argument’s type agree. Compose gets the type fun(fun(t1, t2), fun(fun(t0, t1), fun(t0, t2))), and the proof records every lookup and rule application.

symbolic-derivative.py differentiates formulas held as terms, such as mul(sym('x'), sym('x')), with one backward rule per form: sum, difference, product, quotient, power and logarithm. Results stay unsimplified, so x*x gives 1*x + x*1 and log(log(x)) gives (1/x)/log(x); a product of three factors shows the whole product-rule expansion, and a last goal differentiates y/(x-1), treating y as a constant.

group-inverse-uniqueness.py proves that an element of a group has only one inverse. It assumes x has two inverses, i and j, and states the identity, inverse and associativity laws as forward rules over a product relation product(A, B, AB); associativity alone concludes equal(Left, Right). The program derives same_inverse('x', 'i', 'j') and its mirror, and the checked proof is the textbook chain i = (j·x)·i = j·(x·i) = j·e = j.

After an intentional behavior change, run python tools/update_examples.py 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.