peye
Example decks
peye — reasoning you can see.
Each example comes with a short card deck that explains it for a wide audience: the question it asks, what the program says, what peye 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |