The Flyover AI compass — the eight constructs of the methodology: type, definition, rule, property, choice, optimize, default, constraint Flyover AI
Verifiable reasoning infrastructure · World model development as a discipline
Vol. I Founded 2026 Nebraska
The Casebook

The language, worked
across domains.

Each entry is a small, complete KRML model — one that compiles and solves exactly as shown — paired with the reason it earns a place here. The models are easy to read; their significance is often what an outsider, even an adjacent one, misses. That gap is the point.

i.

Animal Taxonomy

Defaults and exceptions over a hierarchy.

Why it's here. Tweety is the canonical test of defeasible reasoning, and it carries at once what a real policy carries. It builds a small ontology (animals, the kinds beneath them, the individuals beneath those), so classification is hierarchical, and it runs defaults at more than one level of it: animals do not fly; birds, more specifically, do. It then defeats the bird default two distinct ways: a strong exception that asserts the opposite (a penguin does not fly), and a weak one that merely withdraws the presumption (an injured bird, left undetermined). That two-kinds-of-exception difference is the first thing outsiders miss, and it is no technicality: an explicit "no" is not the absence of a "yes," which in a regulation is the difference between a prohibition and a silence. The model is also elaboration tolerant: a new kind, exception, or individual costs nothing already written.

And why it matters now. This is the cleanest line between the methodology and the knowledge graphs in fashion today. A graph holds the taxonomy and the facts; what its standard, monotonic form cannot hold is the defeasible part. "Birds normally fly, a penguin is the exception" is not a default in a classical ontology, it is a contradiction, which is why the penguin is the very example the description-logic literature reaches for to mark the gap. Closing it means extending the graph with the non-monotonic machinery this methodology is founded on.

"Animal" is a type.
"Bird" is a type of animal.
"Cat" is a type of animal.
"Penguin" is a type of bird.
"Parrot" is a type of bird.

[@in]  An animal may be "injured".
[@out] An animal may be "able-to-fly".

[@ref: D.animal-flight] Normally, an animal is not able-to-fly.
Birds are an exception to [D.animal-flight].
[@ref: D.bird-flight] Normally, a bird X is able-to-fly.

Penguins are not able-to-fly.
A bird X is an exception to [D.bird-flight] if X is injured.

"Sylvester" is a cat.    "Sam" is a bird.       "Polly" is a parrot.
"Tweety" is a penguin.   "Rocky" is a parrot.   Rocky is injured.

Result. Sam and Polly fly: the bird default fires. Sylvester the cat does not — the general "animals don't fly" default reaches him. Tweety the penguin does not either, a definite "no." Rocky, an injured parrot, is neither: the default is withdrawn, and nothing asserts he cannot fly.

↑ Contents

ii.

The Eight Queens

Compactness and comprehension, at once.

Why it's here. Eight queens on a board is a combinatorial chestnut; solving it is not the point. The point is an encoding at once tiny and readable. A queen has a column; the diagonals are "column + row" and "column − row"; the rule is that no two queens share the same value for either. The native encodings constraint solvers use for this are just as compact and nearly unreadable to anyone outside the field; this one a layperson can follow. What buys that is treating a queen's column and row as ordinary properties of the object and writing the constraints as plain arithmetic over them, the quiet bridge between how a solver builds terms and how an English speaker does. Most controlled languages never get compactness and comprehension at once; this is where ours does.

Let "n" be 8.

The "queens" (singular: "queen") are named Q[I]
    where I is a "row" from 1 to n.

Every queen has exactly one "column", which is an integer ranging from 1 to n.
[@out] We may choose exactly one column for each queen.

No two queens have the same column.
No two queens have the same value for column + row.
No two queens have the same value for column - row.

Result. One queen per row, at columns 5, 7, 1, 4, 2, 8, 6, 3 — no two sharing a column or a diagonal. One of the puzzle's 92 solutions, found in milliseconds.

↑ Contents

iii.

Einstein's Riddle

Fifteen clues, one solution.

Why it's here. The riddle is fifteen clues in plain English with a single solution, and the demonstration is the fidelity between a clue and its encoding: each clue becomes one constraint that reads almost exactly like the sentence it came from, and the whole puzzle rests on cardinality — exactly one nationality, color, drink, cigarette, and pet per house, each value used exactly once. You can set the model beside the riddle and check it by reading. That is the property a regulation needs and almost never gets from its code.

// --- Attribute types ---
The "nationalities" (singular: "nationality") are:
    "brit", "swede", "dane", "norwegian", and "german".
The "colors" (singular: "color") are:
    "red", "green", "white", "yellow", and "blue".
The "drinks" (singular: "drink") are:
    "tea", "coffee", "milk", "beer", and "water".
The "cigarettes" (singular: "cigarette") are:
    "pall-mall", "dunhill", "blends", "blue-master", and "prince".
The "pets" (singular: "pet") are:
    "dogs", "cats", "birds", "horses", and "fish".

// --- Houses ---
The "positions" (singular: "position") are numbered from 1 to 5.
The "houses" (singular: "house") are named H[I]
    where I is a "position" from 1 to 5.

// --- Properties ---
Every house has:
    exactly one "nationality", which is a nationality; and
    exactly one "color", which is a color; and
    exactly one "drink", which is a drink; and
    exactly one "cigarette", which is a cigarette; and
    exactly one "pet", which is a pet.

// --- Choice rules ---
[@out] We may choose exactly one nationality for each house.
[@out] We may choose exactly one color for each house.
[@out] We may choose exactly one drink for each house.
[@out] We may choose exactly one cigarette for each house.
[@out] We may choose exactly one pet for each house.

// --- Uniqueness ---
No two houses have the same nationality.
No two houses have the same color.
No two houses have the same drink.
No two houses have the same cigarette.
No two houses have the same pet.

// --- Clues ---
// Clue 8: The man in the middle house drinks milk.
H[3]'s drink is milk.

// Clue 9: The Norwegian lives in the first house.
H[1]'s nationality is norwegian.

// Clue 1: The Brit lives in the red house.
For any house X,
    it is required that X's color is red
    if X's nationality is brit.

// Clue 2: The Swede keeps dogs.
For any house X,
    it is required that X's pet is dogs
    if X's nationality is swede.

// Clue 3: The Dane drinks tea.
For any house X,
    it is required that X's drink is tea
    if X's nationality is dane.

// Clue 4: The green house is immediately to the left of the white house.
For any house X and house Y,
    it is required that Y's position == X's position + 1
    if X's color is green, and
       Y's color is white.

// Clue 5: The green house owner drinks coffee.
For any house X,
    it is required that X's drink is coffee
    if X's color is green.

// Clue 6: The person who smokes Pall Mall keeps birds.
For any house X,
    it is required that X's pet is birds
    if X's cigarette is pall-mall.

// Clue 7: The owner of the yellow house smokes Dunhill.
For any house X,
    it is required that X's cigarette is dunhill
    if X's color is yellow.

// Clue 10: The man who smokes Blends lives next to the man who keeps cats.
For any house X and house Y,
    it is required that | X's position - Y's position | == 1
    if X's cigarette is blends, and
       Y's pet is cats.

// Clue 11: The man who keeps horses lives next to the man who smokes Dunhill.
For any house X and house Y,
    it is required that | X's position - Y's position | == 1
    if X's pet is horses, and
       Y's cigarette is dunhill.

// Clue 12: The owner who smokes BlueMaster drinks beer.
For any house X,
    it is required that X's drink is beer
    if X's cigarette is blue-master.

// Clue 13: The German smokes Prince.
For any house X,
    it is required that X's cigarette is prince
    if X's nationality is german.

// Clue 14: The Norwegian lives next to the blue house.
For any house X and house Y,
    it is required that | X's position - Y's position | == 1
    if X's nationality is norwegian, and
       Y's color is blue.

// Clue 15: The man who smokes Blends has a neighbor who drinks water.
For any house X and house Y,
    it is required that | X's position - Y's position | == 1
    if X's cigarette is blends, and
       Y's drink is water.

Result. A single, unique assignment — and the answer the riddle asks for: the German, in the green house, keeps the fish.

↑ Contents

← Back to flyoverlabs.ai