Each example comes with a short card deck that explains it for a wide audience: the question it asks, what the program says, what eyemind 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.
| Deck | What it is about |
|---|---|
| ackermann | The Ackermann function through the hyperoperation sequence, exactly |
| age | Calendar-year and elapsed-day age checks at an explicit reference date |
| alternatives | Alternative routes, disjunction and once |
| audited-grants | A grant policy whose own proof and check report are read back as facts and audited, in the same language |
| aunt-agatha | Who killed Aunt Agatha? A conclusion entailed by holding in every model of the premises |
| backward | Backward definitions inside forward bodies |
| bayes-diagnosis | Normalized probabilities for illustrative printer faults |
| collatz | Parity-based recursive trajectories over a range of starts |
| complex | Complex arithmetic, exact over Gaussian integers and polar beyond them |
| control-system | Feedforward and nonlinear feedback commands for two actuators |
| data-value-right | A right to the value of personal data in the age of AI: how it fits existing EU law, and how it could become an autonomous right |
| deep-taxonomy-10 | A ten-level subclass chain with branches that lead nowhere |
| deep-taxonomy-100 | The same taxonomy benchmark at a hundred levels |
| deep-taxonomy-1000 | The same taxonomy benchmark at a thousand levels |
| deep-taxonomy-10000 | The same taxonomy benchmark at ten thousand levels |
| deep-taxonomy-100000 | The same taxonomy benchmark at a hundred thousand levels |
| delfour | A store scanner gives low-sugar advice from a signed, scoped insight, without learning the household’s diabetes |
| deontic-logic | Obligations, prohibitions and compensation that does not erase a violation |
| dijkstra | Dijkstra’s shortest route over a cost-ordered queue, with every step checked |
| dog-license | A licensing threshold based on collected dog counts |
| easter | Easter Sunday by the anonymous Gregorian algorithm, 2021 to 2050 |
| existential-rules | Existential rules: a fresh witness per activation, never a clash |
| expression-eval | Recursive expression graphs used in forward inference |
| family-cousins | Generations, family branches and cousin relationships |
| fibonacci | Fast doubling for exact Fibonacci numbers, and the golden ratio |
| flat-map | Predicate-based mapping with multiple or missing values |
| four-color | Four-colouring the map of the European Union |
| goldbach | Goldbach splits of every power of two up to 2^25 |
| good-cobbler | Trade-specific classification from structured descriptions |
| gps | Goal-driven parallel sequences: routes to a goal state within duration, cost, belief and comfort limits |
| graphs | Base data, negation and collection |
| group-inverse-uniqueness | Uniqueness of group inverses derived from the associativity, identity and inverse laws |
| hanoi | Recursive construction of a disk-move sequence |
| integrity | A provable integrity violation |
| interval-relations | All thirteen interval relations and endpoint completion |
| inventory | An invoice from collected line totals |
| kaprekar | Every four-digit Kaprekar routine reaches 6174 within seven steps |
| knapsack-optimization | The 0/1 knapsack problem: the most valuable pack within a weight limit |
| lists | Concatenation, mapping and summation |
| lldm | Leg length discrepancy measured from radiograph landmarks, with an alarm and its reason |
| monkey-bananas | Every plan of up to five moves that gets the monkey the bananas |
| nixon-diamond | A default guarded by negation, so a contrary rule takes priority |
| owl-property-chain | A property chain declared as data, followed by one general rule |
| package-holiday | Package holiday cancellations under the tour operator’s ODRL terms and the 2015 and revised EU Package Travel Directive |
| paraconsistent-animals | Local summaries of conflicting observations |
| path-discovery | Full airport network with configurable endpoints and maximum stopovers |
| peano | Symbolic arithmetic, relational addition and a chained derivation |
| peasant | Peasant multiplication and exponentiation by halving and doubling |
| permissions | Role permissions with exclusions |
| policy-risk | Ranked findings with explanations and suggested mitigations |
| polynomial | Complex roots of polynomials up to degree 4 by Cardan and Lagrange |
| queens | Configurable N-queens search with diagonal constraints |
| rdf12-annotated-claims | Conflicting RDF 1.2 annotated claims ranked by confidence and trust, with typed literals read as numbers |
| rdf12-annotation | An RDF 1.2 annotation: an asserted triple recovered with the reifier that records who stated it and when |
| rdf12-directional-language | RDF 1.2 directional language strings keep their base direction through a display rule |
| rdf12-nested-triple-term | Nested RDF 1.2 triple terms: one pattern reaches the triple inside a claim inside a review |
| rdf12-trig-graph-join | Data about a named graph in the default graph joined with data inside that graph |
| rdf12-trig-named-graph | Ancestors derived within a TriG named graph, each conclusion kept in its graph |
| rdf12-trig-triple-term | A triple term inside a named graph, asserted in the graph that holds the claim |
| rdf12-triple-term | An RDF 1.2 triple term: a claim names a triple without asserting it, and accepting the claim asserts it |
| reachability | Finite closure in a graph containing a cycle |
| research-portal | A hospital research portal combines ODRL/DPV policy decisions with Digital Omnibus device consent and breach plans |
| schema-inference | Subclasses, subproperties, domains and ranges |
| scoped-audit | Presence and absence within separate quoted graphs |
| shortest-path | Weighted paths and stratified minimum selection |
| sieve | The sieve of Eratosthenes over an explicit list of integers |
| socrates | Class membership derived through a subclass rule |
| state-transitions | Account balances from an ordered event log |
| strings | Text construction and Unicode inspection |
| superdense-coding | Superdense coding in discrete quantum theory, with interference as odd path counts |
| symbolic-derivative | Symbolic differentiation of structured formulas by the sum, product, quotient, power and chain rules |
| teleportation | Quantum teleportation in discrete quantum theory, checked for every state and outcome |
| terms | Quoted graphs, triple terms and residual witnesses |
| turing | A Turing machine interpreter running a binary incrementer |
| type-inference | Typing rules for a small expression language, run as a checker |
| unification | Open lists and repeated-variable constraints |
| variable-predicates | Relations selected and renamed through data bindings |
| witnesses | Structured witnesses and shared multi-head conclusions |
| wolf-goat-cabbage | The river crossing, with seven crossings shown to be minimal |
| zebra | The zebra puzzle solved by narrowing five partially known houses |