Introduction

Most software that reasons about the world tracks facts: the coin is heads, the marble is in the basket, the robot is in the hall. delhi tracks something harder — what each agent thinks about those facts, what they think everyone else thinks, and how all of that changes when things happen that some agents witness and others miss.

That extra layer is where the interesting failures live:

$ delhi eval examples/sally_anne.delhi \
      -a "sally_leaves()" "anne_moves()" "sally_returns()" \
      -f "B[sally] basket & !basket"
true

Sally believes the marble is in the basket. It is not in the basket. Both at once — and that is not a bug in the model, it is the point. Sally left the room before Anne moved the marble, so her belief is stale rather than wrong-headed, and a system that could not represent the gap could not represent her at all.

Who this is for

Two audiences, and you can skip half of this book depending on which you are.

If you have not met epistemic logic before, start with Possible worlds. Four short chapters cover what it means to say an agent "knows" or "believes" something formally, why those two words need separate machinery, and what happens to both when the world changes. No prior logic is assumed beyond and, or, not.

If you know the field already, skip to Install and Your first domain. delhi implements mB+, a plausibility-model semantics from Buckingham's thesis extended with safe and conditional belief; the Related systems chapter places it against DEL, mA*, EFP and PDKB, and says plainly what is transcription and what is new.

What delhi is

A model checker, a small declarative language, and a browser UI for exploring both.

• A language. A .delhi file declares agents, propositions, what is true and believed at the start, and a set of actions. It reads like a description of a scenario rather than a set of equations.
• A model checker. Given that file, delhi builds a plausibility model and answers questions about it — including questions three or four levels deep, like "does Alice believe that Bob knows whether Carol is lying".
• A tool. A single self-contained binary. delhi eval for one question, delhi ask to enumerate every formula of a given shape that holds, delhi repl to poke at a scenario, delhi gui for a browser view of the model as it changes.

What delhi is not

A planner. delhi tells you what holds in a state and how a state changes when you apply an action you name. It does not search for a sequence of actions that would achieve a goal. That is the obvious next thing to build on top, and the pieces for it exist, but it is not here yet.

It is also not a theorem prover. Questions are answered against a specific finite model, not proved valid across all models.

A word on the name

delhi is a Rust reimplementation of mecaPlanner, a Java epistemic planner. The semantics, the action types, and several examples come from that lineage; the language, the query system, the tooling and the performance work do not. Where this book states something as delhi's own rather than inherited, it says so.

Possible worlds

The whole field rests on one move. To say what an agent knows, do not describe the agent's head — describe the situations it cannot rule out.

The move

Suppose a coin has been flipped and covered. It landed heads. Alice did not see it.

We could try to model Alice's ignorance by giving her a "knows-heads" flag set to false. That works until you ask a second question — does she know it is tails? Also false. Does she know it is heads-or-tails? True. Three flags now, and they have to be kept consistent with each other by hand.

Instead, list the situations Alice considers possible:

    w1: heads          w0: tails

She cannot tell them apart, so both are live for her. Now every question answers itself:

• Does Alice know it is heads? Only if heads is true in every world she considers possible. It is false in w0, so no.
• Does she know it is heads-or-tails? That holds in both, so yes — for free, with no extra bookkeeping.
• Is she ignorant of which? Yes: neither heads nor ¬heads holds throughout.

The consistency comes from the structure rather than from discipline. That is the payoff.

The three parts

A model is three things:

• Worlds — the situations in play. One of them is the actual one; the rest are there because somebody cannot rule them out.
• A valuation — which propositions are true in each world.
• A relation, per agent — which worlds that agent connects to which. Alice's relation links w1 and w0 because she cannot distinguish them.

Each agent gets its own relation. That is what lets Bob know the coin while Alice does not: Bob's relation links each world only to itself, so from w1 he sees only w1.

state {
  *w1 <- { heads }      // `*` marks the actual world
   w0 <- { }
  alice: w0 ~ w1        // alice cannot tell these apart
}                       // bob relates each world only to itself

That is real delhi syntax — delhi show prints models in exactly this form. Bob needs no line at all: with nothing declared, he distinguishes everything.

Reading the picture

Two habits to build, because they are what make the diagrams say anything.

Knowledge is what survives every arrow. To evaluate "Alice knows φ", stand in the actual world, follow every one of Alice's arrows, and check φ in each place you land. One counterexample is enough to defeat the claim. This is why knowledge is expensive: it takes all the possibilities agreeing.

More arrows mean less knowledge. An agent who connects everything to everything knows nothing beyond what is true everywhere. An agent whose arrows go only from each world to itself knows the actual world exactly. Learning something means deleting arrows.

That second habit is worth sitting with, because it inverts the intuition. Information does not add to the model. It cuts it down.

Where this is going

So far every arrow has meant "cannot tell these apart" — a symmetric, all-or-nothing sort of uncertainty. That gives you knowledge, and only knowledge.

Belief needs more, because a believer is not merely uncertain: they lean. Alice may consider tails possible while finding heads far more plausible, and if you tell her the coin was tails she should be able to change her mind without ever having been logically wrong. Plain arrows cannot express leaning.

The next chapter adds the missing structure — an ordering on the arrows — and shows why knowledge and belief end up obeying genuinely different laws.

Knowledge and belief

English uses "know" and "believe" almost interchangeably. Logic cannot, because the two obey different laws — and the difference is exactly what makes a system able to model an agent that is confidently wrong.

The one law that separates them

Knowledge is factive. Belief is not.

If Alice knows the coin is heads, then the coin is heads. If Alice merely believes it, the coin may well be tails. Written out:

K[alice] h  →  h        holds always
B[alice] h  →  h        does NOT hold

Everything else follows from taking that seriously. A system with only one attitude has to pick: make it factive and you cannot model mistakes, or make it non-factive and you cannot model anything an agent has actually established.

Adding the leaning

The previous chapter gave each agent a relation meaning "cannot tell these apart". To get belief, delhi replaces it with an ordering: not just which worlds are possible, but which are more plausible.

carol: w0 < w1

Read it left to right: w1 is at least as plausible as w0. Plausibility increases along the arrow, and in the surface syntax it increases to the right.

This direction is worth pinning down, because an inverted ordering is still a perfectly valid model — nothing will complain, and every answer will be subtly backwards.

From that one ordering, both attitudes fall out:

Carol considers both w0 and w1 possible, so she does not know which. But w1 is her most plausible world, so whatever is true there is what she believes.

What each obeys

The two attitudes end up satisfying different axiom systems. You do not need these to use delhi, but they are the standard names and they say precisely what each attitude promises:

Knowledge is S5.

• K[a] φ → φ — what you know is true (factivity)
• K[a] φ → K[a] K[a] φ — you know what you know (positive introspection)
• ¬K[a] φ → K[a] ¬K[a] φ — you know what you don't know (negative introspection)

Belief is KD45. The same introspection, and consistency in place of factivity:

• B[a] φ → ¬B[a] ¬φ — you never believe a thing and its negation (consistency)
• B[a] φ → B[a] B[a] φ, ¬B[a] φ → B[a] ¬B[a] φ — introspection, as above

Notice what belief keeps: an agent can be wrong, but not incoherent. Sally believes the marble is in the basket when it is not; she does not simultaneously believe it is not.

delhi verifies these as frame properties rather than assuming them — see Operators.

Two more, and why

Knowledge and belief are the two you will reach for. delhi carries two more because the gap between them turns out to be where the useful questions live.

Safe belief, [][a] φ — true in every world at least as plausible as the current one. It sits between the other two: stronger than belief, weaker than knowledge. Its point is stability — a safe belief survives learning any true fact, where a mere belief can be overturned by one.

It is measured from the actual world rather than from a fixed set, which gives it a character quite unlike the other two and makes it the subject of its own chapter: Safe belief.

Conditional belief, B^ψ[a] φ — what the agent would believe if it learned ψ. This is the one that makes revision predictable: you can ask what Alice's belief would become before telling her anything, and the answer is already determined by her ordering.

$ delhi eval examples/coin_lie.delhi -f "B[carol] h"        # believes heads
true
$ delhi eval examples/coin_lie.delhi -f "B^(!h)[carol] h"   # ...but would give it up
false

An agent that could not be told anything is not a believer, just a fact table with extra steps. Conditional belief is what encodes the difference.

The whole point

Put the pieces together and you can express a state no purely fact-based system can:

B[carol] h  &  !h  &  K[alice] !h

Carol believes heads, it is tails, and Alice knows it is tails. Three agents, one coin, and a disagreement that is not a contradiction — because belief is not factive, and each agent's ordering is its own.

The next chapter goes one level up: what Alice believes about what Carol believes, and why that is where the genuinely hard cases start.

Higher-order attitudes

Everything so far has been first-order: what an agent thinks about the world. The interesting cases are one level up — what an agent thinks about what another agent thinks.

Nesting

The operators nest, and that is all there is to the syntax:

K[alice] h                          alice knows the coin is heads
B[alice] K[bob] h                   alice believes bob knows it
B[alice] B[bob] B[carol] !h         alice thinks bob thinks carol thinks it is tails

Semantically nothing new happens. B[alice] B[bob] h means: in every world Alice finds most plausible, B[bob] h holds — which in turn means that in every world Bob finds most plausible from there, h holds. Follow the arrows, then follow more arrows.

What is new is that these can come apart from the first-order facts in ways that matter.

The false-belief task

Developmental psychology has a canonical test for whether a child can represent someone else's mind separately from reality. It is called Sally-Anne, and it runs like this:

Sally puts her marble in the basket and leaves the room. While she is gone, Anne moves the marble to the box. Sally comes back.

Where will Sally look for her marble?

The answer is the basket. Children under about four say "the box" — they know where the marble is, and they have no machinery for a belief that is false. Getting it right requires holding two incompatible pictures at once: where the marble is, and where Sally thinks it is.

That is exactly the structure of examples/sally_anne.delhi:

$ delhi eval examples/sally_anne.delhi \
      -a "sally_leaves()" "anne_moves()" "sally_returns()" \
      -f "B[sally] basket & !basket"
true

The conjunction is the whole task. !basket is the world; B[sally] basket is Sally. Neither is negotiable and they disagree.

The single clause that makes it work is in the action that moves the marble:

sally observes if present

Sally sees Anne's move only if she is in the room — and sally_leaves() has already made present false. Take the condition away and the whole phenomenon vanishes: she witnesses the move and updates like anyone else.

Second-order false belief

Now go one level further. It is possible to be wrong not about the world, but about someone else's mind — and to be right about the world at the same time.

examples/coin_lie.delhi builds exactly that. Alice lies that the coin is tails, Bob distracts her, Carol peeks and learns the truth. Alice, being distracted, never sees the peek happen, so her picture of Carol goes stale:

$ delhi eval examples/coin_lie.delhi \
      -a "announce_not_heads()" "distract_a()" "peek_c()" \
      -f "B[alice] B[carol] !h & K[carol] h"
true

Alice believes Carol believes tails. Carol knows heads. Alice is not mistaken about the coin — she is mistaken about Carol.

This is where the possible-worlds machinery earns its keep. There is no flag you could set that would represent "Alice's model of Carol is two events out of date"; it falls out of Alice's arrows pointing at worlds where the peek never happened.

Common knowledge

One more operator, and it is not just "everybody knows".

C[*] φ — common knowledge — means everyone knows φ, and everyone knows that everyone knows it, and so on without end. It is the standard precondition for coordination: you and I can meet at noon without further discussion only if the arrangement is common knowledge, not merely known to us both.

The infinite regress is not a problem to compute. C is evaluated over the transitive closure of every agent's relation at once: φ is common knowledge exactly when it holds in every world reachable by any chain of any agents' arrows.

examples/muddy_children.delhi is the classic demonstration. Three children can each see the others' foreheads but not their own. The father announces "at least one of you is muddy" — telling nobody anything they did not already see. But it makes the fact common, and that alone lets them deduce their own state after two rounds of nobody speaking up.

$ delhi state examples/muddy_children.delhi \
      -a "father_speaks()" "nobody_knows()" "nobody_knows()"

undecided becomes believes. Nothing was said in those last two rounds — the silence was the information.

What to take away

Higher-order attitudes are not a decoration on top of the first-order ones. They are where lying, deception, coordination, teaching and pretence all live, and every one of them requires an agent's model of another agent to be able to go stale or be wrong.

The next chapter covers how these attitudes change when something happens — which, given that staleness is the whole story here, is where the observability rules turn out to matter more than anything else.

How attitudes change

A static model says what agents think right now. The field is called dynamic epistemic logic because the real subject is what happens next — and specifically, how one event can leave different agents in different epistemic positions.

The core idea

An event is modelled the same way a state is: as a little model of its own. It has events in place of worlds, a precondition on each saying when it can occur, and one relation per agent saying which events that agent cannot tell apart.

Then the new state is the product of the two. Every (world, event) pair whose precondition holds becomes a new world, and an agent connects two new worlds when it connected both the worlds and the events they came from.

That product is the entire mechanism. Announcements, sensing, lying, and acting unobserved are all the same operation with different little models.

Three kinds of thing that can happen

delhi gives you three, because they change different things:

The distinction between the last two is the factivity line from Knowledge and belief. Looking in the box tells you how things are; being told is only as good as the teller.

peek_c() {
    actor      carol
    determines h          // she looks: she will KNOW
    carol observes
}

announce_not_heads() {
    actor     alice
    announces !h          // she says it: hearers will BELIEVE
    alice observes, bob observes, carol observes
}

announces !h does not require !h to be true. That is what makes it a lie rather than a fact, and it is why the hearer ends up believing something false while still not knowing it.

Who saw it

This is the part that does the work, and it is where most of the interesting modelling lives. Three positions an agent can be in:

The middle one is easy to overlook and does a great deal. If Bob peeks into a box and Alice is aware, Alice does not learn the coin — but she learns that Bob has. She comes to know that he knows whether:

$ delhi eval examples/coin_lie.delhi -a "distract_a()" "peek_c()" -f "K[bob] Kw[carol] h"
true      # bob heard the peek: he knows carol settled it
$ delhi eval examples/coin_lie.delhi -a "distract_a()" "peek_c()" -f "K[alice] Kw[carol] h"
false     # alice was distracted: she does not even know it happened

Mechanically, a sensing or announcing action builds three events — ψ, ¬ψ, and a ⊤ event standing for nothing observable happened. Each agent gets two edge labels:

• ψ ↔ ¬ψ is labelled ¬observes(i)
• the edges to the ⊤ event are labelled ¬(observes(i) ∨ aware(i))

An aware agent keeps the first — the outcomes stay indistinguishable — and loses the second. That is precisely "I know it happened, I don't know how it went". An oblivious agent keeps both and cannot rule out that the world simply carried on.

Conditions make this dynamic. alice aware if !d means her class depends on the state at the time, which is how one distract_a() earlier in the trace turns her from aware into oblivious.

Why belief revision needs the ordering

When an agent learns something that contradicts what it believed, it must not simply be left with nothing. The plausibility ordering from Knowledge and belief is what makes this work: an announcement does not delete the worlds where the announcement is false, it reorders them, promoting the ones consistent with what was said.

The agent's knowledge does not change — every world it considered possible is still possible. Only the leaning moves. And because the disfavoured worlds are still there, a later truthful announcement can promote them back:

$ delhi eval examples/coin_lie.delhi -a "announce_not_heads()" -f "B[carol] !h"
true      # the lie landed
$ delhi eval examples/coin_lie.delhi -a "announce_not_heads()" "peek_c()" -f "K[carol] h"
true      # she looks, and recovers the truth

A system that deleted worlds on announcement would have made the first step irreversible. Carol would have been stuck believing the lie with no way back, which is not what happens when someone lies to you and you then check.

Models grow — and what to do about it

Product update multiplies. Each action crosses every world with every distinguishable event, so an uncontracted model grows exponentially:

cycle      worlds      cumul
    1          16     72.9us
    2         128      2.2ms
    3        1024    133.6ms
    4        8192      9.47s

The fix is bisimulation contraction: worlds that no agent can distinguish, and that no formula could tell apart, are merged. delhi contracts after every action, which in most domains holds the model at a fixed point — Coin Lie settles at 16 worlds whether you run 2 cycles or 8, taking about 0.6 ms each.

It is not a fixed point in general. Grapevine's cycle creates a genuinely new distinction every time round, because each repetition adds another layer of who-was-present-for-what, and contraction cannot merge what is really different. See the benchmark section of the README for numbers.

Where to go next

You now have the whole conceptual picture: worlds, an ordering, two attitudes plus two refinements, nesting, and product update against three observer classes.

Your first domain builds one from scratch.

Safe belief

Knowledge is what holds everywhere the agent considers possible. Belief is what holds where it considers most plausible. Between them sits a third attitude that turns out to be the interesting one, and the one hardest to guess at from its name.

Everything below is examples/safe_belief.delhi, so you can run it.

Three nested sets

All three operators read φ off a set of worlds. The sets are nested:

        ┌───────────────────────────────────────┐
   K    │  every world the agent can't rule out  │
        │   ┌─────────────────────────────────┐  │
   □    │   │  worlds at least as plausible    │  │
        │   │      as the actual one           │  │
        │   │      ┌───────────────────┐       │  │
   B    │   │      │  the most         │       │  │
        │   │      │  plausible ones   │       │  │
        │   │      └───────────────────┘       │  │
        │   └─────────────────────────────────┘  │
        └───────────────────────────────────────┘

A bigger set is a stronger claim, so K[a] φ → □[a] φ → B[a] φ, and both arrows are strict.

It depends where you are standing

K and B are anchored to fixed sets — the whole class, the top of the ordering. □ is measured from the actual world, and that one difference is what gives it its character.

Three agents, one question, none of whom knows the answer:

initially {
    up                      // the server really is up
    ?[ada] up   B[ada] up   // ada cannot tell, but leans the right way
    ?[ben] up   B[ben] !up  // ben cannot tell, and leans the wrong way
    ?[cleo] up              // cleo has no leaning either way
}

$ delhi eval examples/safe_belief.delhi -f "[][ada] up"     # true
$ delhi eval examples/safe_belief.delhi -f "[][ben] !up"    # false
$ delhi eval examples/safe_belief.delhi -f "[][cleo] up"    # false

Plain belief cannot separate these — all three hold their views equally firmly, and B[ada] up and B[ben] !up are both true. Safe belief separates them at once:

• Ada is right. The actual world is already her most plausible one, so there is almost nothing ranked above it, and her belief survives everything.
• Ben is wrong. His favoured worlds sit above reality in his own ordering, and !up has to hold in those too. It does not.
• Cleo has no leaning. Both worlds are equally plausible to her, so both sit above the actual one, and nothing non-trivial is safe.

A consequence worth naming: □ is factive. □[a] φ → φ. You cannot safely believe something false, because the actual world is always in the set being checked. Belief has no such guarantee — that is the whole point of belief.

What it actually means: undefeated by truth

The definition is geometric, but the characterisation is not:

A safe belief is one that no true information can overturn.

Watch it. gossip() announces up, which is true:

$ delhi eval examples/safe_belief.delhi -a "gossip()" -f "[][ada] up"     # true — untouched
$ delhi eval examples/safe_belief.delhi -a "gossip()" -f "B[ben] up"      # true — overturned

Ada's belief was safe, and the truth left it alone. Ben's was not, and one true sentence flipped it. That is not a coincidence about this domain — it is what □ means.

The conditional-belief operator says the same thing without running anything:

$ delhi eval examples/safe_belief.delhi -f "B^up[ben] !up"     # false

Ben would give up !up on learning up. His belief was defeasible, and □ is exactly the operator that says so.

Undefeated by truth, not undefeated. A safe belief can still be broken by a falsehood — see A lie can destroy one below. □ promises stability against true information, and nothing more.

How an agent acquires one

An agent safely believes φ exactly when the actual world outranks every world where φ fails. Three ways to get there:

The middle row is the one to sit with. A truthful announcement took Ben from a wrong belief to a safe one — without giving him knowledge. He is now right, and nothing true can shake him, yet he still cannot rule out the alternative. That state has no name in ordinary English, and it is what □ is for.

The bottom row can never come out otherwise. A lie moves belief and can never make it safe, because □ is factive.

There is also a fourth, passive route: already being right. Ada acquired nothing. Her belief was safe from the first line of the file, because it happened to match the world.

A lie can destroy one, just not create one

$ delhi eval examples/safe_belief.delhi -f "[][ada] up"              # true
$ delhi eval examples/safe_belief.delhi -a "deny()" -f "[][ada] up"  # false

Safe belief is not permanent. deny() is false, and it still reorders Ada's worlds enough to destroy the safety of a belief she had held safely. Being undefeatable by truth is no protection at all against a convincing falsehood.

Can an agent tell that its belief is safe?

Here the answer is genuinely surprising, and it is where □ differs most from the other two.

No. K[a] □[a] φ and K[a] φ are equivalent.

$ delhi eval examples/safe_belief.delhi -f "K[ada] [][ada] up"   # false

Ada's belief is safe, and she cannot establish that it is. The reason is short: K quantifies over every world she cannot rule out, including her least plausible one — and from there, "everything at least as plausible" is the entire class. So K□φ demands φ throughout, which is just Kφ.

So an agent can never know it holds a safe belief that falls short of knowledge. Safe belief and knowledge become certifiable at exactly the same moment.

But the agent is not in the dark. It is overconfident.

$ delhi eval examples/safe_belief.delhi -f "B[ada] [][ada] up"     # true
$ delhi eval examples/safe_belief.delhi -f "B[ben] [][ben] !up"    # true  ← but it is NOT

B[a] □[a] φ and B[a] φ are equivalent: every agent believes every one of its beliefs is safe. From the top of your own ordering, everything looks unshakeable — that is what being at the top means. Ben believes his belief is undefeatable, while one true sentence is about to overturn it.

Third form, and this one behaves:

$ delhi eval examples/safe_belief.delhi -f "[][ada] [][ada] up"    # true
$ delhi eval examples/safe_belief.delhi -f "[][ben] [][ben] !up"   # false

□[a] □[a] φ ↔ □[a] φ. Safe belief is safely introspective, because the plausibility relation is a preorder — transitivity gives one direction, reflexivity the other.

What that means for modelling

□ is, in a real sense, an outside observer's operator. It measures the fit between an agent's ranking and the way things actually are, and the agent has no access to the second half of that. Its self-report is useless, because it always says yes.

• To let an agent verify its belief is stable, it needs knowledge — sensing, not testimony.
• To find out yourself whether a belief is stable, ask □[a] φ from outside. That is the modeller's question, and the agent cannot answer it for you.

This is a genuine asymmetry with the other two operators, both of which an agent introspects on perfectly: K is S5 and B is KD45, and both carry positive and negative introspection.

Why the operator exists at all

K here is S5 — infallible certainty, true in every world the agent cannot rule out. Many epistemologists think that is too strong for the English word knows, and propose instead:

knowledge is true belief that no further truth would overturn.

That is the defeasibility analysis of knowledge (Lehrer & Paxson; Stalnaker), and it is exactly □. Safe belief is not a technical curiosity wedged between two real operators — it is a serious candidate for what knowing is, sitting in the same model as the certainty reading so you can ask for either and compare.

Baltag and Smets, whose plausibility models delhi's semantics are built on, introduce □ for precisely this reason. See Further reading.

Install

delhi is a single self-contained binary. Pick whichever route asks least of you.

From crates.io

Needs a Rust toolchain (rustup.rs), and compiles in a couple of minutes. Installs into ~/.cargo/bin, which rustup already puts on your PATH.

cargo install delhi            # install
cargo install delhi --force    # update to the newest release

--force is how you update: without it, cargo declines to overwrite an existing install.

A prebuilt binary

No Rust needed. Download the archive for your platform from Releases, unpack it, and put delhi somewhere on your PATH. Each archive carries the binary, the examples, the Python wrapper, and both licences, with SHA256SUMS published beside it.

Or let a script do it — it verifies the checksum and unpacks to ~/.local/bin (%LOCALAPPDATA%\delhi\bin on Windows). Neither script edits your shell profile; each reports whether the directory is on PATH and leaves the change to you.

curl -fsSL https://raw.githubusercontent.com/vasanthsarathy/delhi/master/install.sh | sh

irm https://raw.githubusercontent.com/vasanthsarathy/delhi/master/install.ps1 | iex

From source

git clone https://github.com/vasanthsarathy/delhi && cd delhi
cargo install --path crates/delhi

Check it worked

delhi --version
delhi --help

If you installed a prebuilt archive, the examples are beside the binary. If you installed with cargo there is no examples/ directory — but the ten examples are compiled into the binary, so delhi gui can still open them from anywhere.

As a library

The semantics and the language are separate crates, usable without the CLI:

[dependencies]
delhi-lang = "0.1"     # parse, check and query .delhi source
delhi-mb  = "0.1"      # the model checker itself

All the library crates have zero external dependencies. See docs.rs/delhi-lang.

Minimum Rust version

1.78, checked in CI. That is a promise about using delhi — building its own test suite wants something newer, because a test-only dependency does.

A note on version numbers

crates.io history starts at 0.1.4. Versions before that exist as GitHub releases and git tags, but were never published: the binary package was named delhi-cli until 0.1.4, and delhi-gui could not be packaged at all — it reached outside its own directory for the bundled examples, which cargo will not carry into a tarball.

So cargo install delhi@0.1.2 finds nothing, while the prebuilt archives on Releases go back to 0.1.0. From 0.1.4 onward the git tag and the published crate are the same thing.

Your first domain

We will build a scenario from nothing, one piece at a time, and end up with a second-order false belief — an agent that is wrong not about the world but about someone else's mind.

The story: Ana is planning a surprise party for Cleo. Ben knows. Cleo suspects something and might go and check.

Create party.delhi and follow along.

1. Who and what

Every file starts by declaring its vocabulary.

types   { Actor - Object }
objects { ana, ben, cleo - Actor }
agents  { ana, ben, cleo }
props   { party }

• types — a small type hierarchy. Actor - Object reads "Actor is a kind of Object".
• objects — the things that exist, each with a type.
• agents — which of them have minds. Only these can appear inside K[…] or B[…].
• props — the propositions. Here just one: whether a party is being planned.

2. What is true, and who knows it

initially {
    party
    ?[cleo] party
}

actions {}

initially is declarative. You state facts and attitudes, and delhi constructs a model satisfying them — then checks the model against every line you wrote.

• party — a bare proposition is a fact about the actual world.
• ?[cleo] party — Cleo cannot tell whether there is a party. ? is the ignorance operator.

Anything not mentioned is known by everyone, so Ana and Ben know about the party without being named.

actions {} is required even when empty. Leave it out and you get missing required section 'actions'.

Check it:

$ delhi check party.delhi
ok: 1 atoms, 3 agents, 0 ground actions, 2 worlds

Two worlds — one where the party is on, one where it is not. Cleo's ignorance is what created the second. delhi state shows the consequences:

$ delhi state party.delhi
actual world party

  ana   knows party
  ben   knows party
  cleo  undecided party

And delhi show prints the model itself:

state {
   w0 <- {  }
  *w1 <- { party }

  cleo: w0 ~ w1
}

* marks the actual world. Cleo relates the two, so she cannot tell them apart. Ana and Ben need no line at all — with nothing declared they distinguish everything, which is exactly what knowing means.

3. Things that happen

Now the actions. Add a second proposition and three of them:

props   { party, suspicious }

goal { K[cleo] party }

actions {
    ana_denies() {
        actor     ana
        announces !party
        ana observes, ben observes, cleo observes
    }

    ben_hints() {
        actor  ben
        causes suspicious
        ana observes, ben observes, cleo observes
    }

    cleo_checks() {
        actor      cleo
        determines party
        cleo observes
        ben  aware
        ana  aware if !suspicious
    }
}

Three actions, three different kinds of change:

• announces !party — Ana says there is no party. She is lying, and nothing requires otherwise. Hearers come to believe.
• causes suspicious — Ben changes the world.
• determines party — Cleo goes and looks. An observer comes to know.

And three observer positions in cleo_checks():

• cleo observes — she sees the outcome.
• ben aware — he notices her checking but not what she found.
• ana aware if !suspicious — she only notices if she is not preoccupied. Ben's hint sets suspicious, so after ben_hints() this clause drops and Ana is oblivious.

That last line is the hinge of the whole scenario.

4. Watch it happen

Apply the lie alone:

$ delhi state party.delhi -a "ana_denies()"
actual world party, !suspicious

  ana   knows party, !suspicious
  ben   knows party, !suspicious
  cleo  knows !suspicious   believes !party

The lie landed. Cleo believes there is no party — and note she does not know it, because knowledge is factive and there is a party. Being lied to moves belief without touching knowledge.

Now the whole sequence:

$ delhi state party.delhi -a "ana_denies()" "ben_hints()" "cleo_checks()"
actual world party, suspicious

  ana   knows party, suspicious
  ben   knows party, suspicious
  cleo  knows party, suspicious

Cleo checked and now knows. First-order, everyone agrees — the state view is first-order by construction, so it looks like nothing interesting happened.

5. The interesting part

The disagreement is one level up, where the state view cannot show it:

$ delhi eval party.delhi -a "ana_denies()" "ben_hints()" "cleo_checks()" \
      -f "K[ben] Kw[cleo] party"
true
$ delhi eval party.delhi -a "ana_denies()" "ben_hints()" "cleo_checks()" \
      -f "K[ana] Kw[cleo] party"
false
$ delhi eval party.delhi -a "ana_denies()" "ben_hints()" "cleo_checks()" \
      -f "B[ana] B[cleo] !party"
true

There it is. Ben was aware, so he knows Cleo settled the question — without knowing what she found. Ana was oblivious, because Ben's hint had made her suspicious and her aware if !suspicious clause dropped. So Ana's picture of Cleo is two events out of date: she still believes Cleo believes the lie.

Ana is not wrong about the party. She is wrong about Cleo.

6. Let delhi find it for you

You had to guess that formula. ask searches instead — _ is a hole to fill:

$ delhi ask party.delhi -a "ana_denies()" "ben_hints()" "cleo_checks()" \
      -q "B[ana] B[cleo] _"
  B[ana] B[cleo] (!party)
  B[ana] B[cleo] (suspicious)
2 of 4 candidates at depth 0

Better, ask what Ana believes that is not so, with the hole appearing twice:

$ delhi ask party.delhi -a "ana_denies()" "ben_hints()" "cleo_checks()" \
      -d 1 -q "B[ana] _ & !_"
  B[ana] (B[cleo] !party) & !(B[cleo] !party)
1 of 28 candidates at depth 1

One false belief, found rather than guessed: Ana believes Cleo believes there is no party, and Cleo believes no such thing. -d 1 allows one level of modal nesting in the candidates, which is what lets the hole be filled by B[cleo] !party rather than a bare proposition.

What you built

• Two worlds from a single ?
• A lie that moved belief without touching knowledge
• A conditional observer clause that turned one agent oblivious mid-trace
• A second-order false belief, and a query that discovers it

Next: Actions and who sees them for the full observability rules, or Asking questions for what ask can do.

Actions and who sees them

An action declaration has three parts: who does it, what changes, and who notices. The third is where most modelling effort actually goes.

peek_c() {
    actor      carol       // who performs it
    determines h           // what changes
    carol observes         // who notices, and how much
    bob   aware
    alice aware if !d
}

Parameters

Actions can be parameterised over declared objects. Every well-typed grounding is generated, and any whose precondition folds to false is dropped before it is built:

move(?who, ?from, ?to) {
    actor  ?who
    pre    at(?who, ?from) & adjacent(?from, ?to)
    causes at(?who, ?to), !at(?who, ?from)
    ?who observes
}

Ground names are what you pass to -a: move(alice,hall,study).

What changes

An action has exactly one of these. pre φ guards any of them.

Why determines is propositional only. Sensing settles a fact by looking at the world, and there is nothing in the world to look at that would settle K[bob] p. If you want an agent to learn about another's mind, that is announces — someone tells them — or aware, which is the subject of the rest of this chapter.

Who notices

Both clauses take a condition — alice aware if !d — which is evaluated in the state at the time, so an agent's class can change during a trace.

What aware buys you

It is the class people skip, and it does the most interesting work. An aware agent learns that the actor settled something, without learning what:

$ delhi eval examples/coin_lie.delhi -a "distract_a()" "peek_c()" -f "K[bob] Kw[carol] h"
true      # bob heard the peek, so he knows carol knows whether
$ delhi eval examples/coin_lie.delhi -a "distract_a()" "peek_c()" -f "K[alice] Kw[carol] h"
false     # alice was distracted: she does not know it happened at all
$ delhi eval examples/coin_lie.delhi -a "distract_a()" "peek_c()" -f "?[alice] Kw[carol] h"
true      # she cannot even say whether carol knows

Three agents, one action, three genuinely different epistemic positions.

How it works. A sensing or announcing action builds three events: ψ, ¬ψ, and a ⊤ event meaning nothing observable happened. Each agent gets two labels:

• ψ ↔ ¬ψ labelled ¬observes(i) — can the agent tell the outcomes apart?
• edges to ⊤ labelled ¬(observes(i) ∨ aware(i)) — can it tell that anything happened?

observes loses both. aware keeps the first and loses the second. Oblivious keeps both.

An agent cannot be in two classes

Declaring the same agent as both observes and aware is an error. This matters for parameterised actions, where a naive grounding easily produces both:

peek(?p) {
    actor      ?p
    determines h
    ?p observes
    ?o aware if !same(?p, ?o)      // every OTHER agent
}

Without that guard, grounding ?o to ?p would put the peeker in both classes. A clause whose condition folds to ⊥ is dropped rather than recorded, which is what makes the guarded form legal.

Invariants

Constraints that must hold in every state, not only the first:

invariants { !((B[a] p & B[b] !p) | (B[a] !p & B[b] p)) }

Checked when the initial state is built and after every action. check refuses a domain inconsistent with its own constraint, step exits 1, and the REPL reports and carries on — exploring past a break is usually what you want.

Asking questions

Three ways, depending on how much you already know about what you are looking for.

All three take -a ACTION… to run a trace first, and all three exist at the REPL prompt and in the browser console as a bare formula, :ask, and :state.

eval

$ delhi eval examples/coin_lie.delhi -a "peek_c()" -f "K[bob] Kw[carol] h"
true

Exit code 0 if it holds, 1 if not, 2 if the formula is malformed — so a shell can branch on the answer, and a typo never looks like a refutation.

Any mB+ formula works: the operators, nested arbitrarily, closed under &, |, !.

ask

ask takes a pattern with _ marking a hole, and reports every formula of that shape that holds:

$ delhi ask examples/coin_lie.delhi -q "B[carol] _"
  B[carol] (!d)
  B[carol] (h)
2 of 4 candidates at depth 0

The hole is filled from the modal literals of the domain — each proposition and its negation, then attitudes about those, and so on. -d N sets how deep that nesting may go.

The hole may appear more than once, and all occurrences are filled with the same formula. That is what makes the interesting recipes possible:

The false-belief recipe is the one to try first, because it finds things you would not have thought to check.

Depth costs. Candidates grow fast — the count is reported so you can see it, and the answer says truncated if the search hit its cap. Start at 0 or 1.

state

$ delhi state examples/coin_lie.delhi -a "announce_not_heads()"
actual world !d, h

  alice  knows !d, h
  bob    knows !d, h
  carol  knows !d   believes !h

First-order by construction — one line per agent, one attitude per proposition. Nested attitudes do not fit that shape and are not shown; use eval or ask for those.

The three lists partition the propositions: every proposition is in exactly one of knows, believes, undecided for each agent.

Ignorance and "knows whether"

Two sugar forms worth knowing, because they are what you actually want more often than K:

• Kw[a] φ — knows whether: K[a] φ | K[a] !φ. The agent has settled the question, either way.
• ?[a] φ — ignorance: !Kw[a] φ. The agent has not.

Bw and ?? are the belief-level counterparts. Both genuinely need the disjunction — "knows whether" is not expressible without it, which is why they exist as operators rather than as something you write out each time.

Machine-readable output

Every one of these takes --json, which emits exactly one object on stdout, errors included:

$ delhi eval examples/coin_lie.delhi -f "B[carol] h" --json
{"ok":true,"value":true}

See From Python.

From Python

Most epistemic-reasoning work sits inside an ML or cognitive-modelling stack written in Python. python/delhi.py wraps the CLI: standard library only, nothing to install. It ships inside every release archive, or take it from the repository.

Put delhi on your PATH, drop the file beside your code:

from delhi import Domain

d = Domain("examples/coin_lie.delhi")
d.do("distract_a()", "peek_c()")          # apply a trace

d.eval("K[bob] Kw[carol] h")              # True  — bob heard the peek
d.eval("K[alice] Kw[carol] h")            # False — alice was distracted
d.eval("?[alice] Kw[carol] h")            # True  — she cannot even say

s = d.state()
s.facts                                   # ['d', 'h']
s.agents[0].agent, s.agents[0].knows      # ('alice', ['d', 'h'])

d.reset().do("announce_not_heads()", "distract_a()", "peek_c()")
d.ask("B[alice] B[carol] _")              # ['B[alice] B[carol] (d)',
                                          #  'B[alice] B[carol] (!h)']
d.eval("B[alice] B[carol] !h & K[carol] h")   # True — the false belief

What the API gives you

Two behaviours worth knowing. Domain replays the trace from the initial state on every call rather than holding a live model, so undo() is exact and two Domains over one file cannot drift. And a malformed formula raises rather than returning False — a typo must not read as a refuted hypothesis.

Underneath

Every command takes --json and emits exactly one object on stdout, errors included, so a caller never has to decide whether what it read was an answer or a diagnostic:

$ delhi eval examples/coin_lie.delhi -f "B[carol] h" --json
{"ok":true,"value":true}
$ delhi eval examples/coin_lie.delhi -f "K[nobody] h" --json
{"ok":false,"error":"1:1: `nobody` is not a declared agent\n  K[nobody] h\n  ^^^^^^^^^^^"}

Exit codes are unchanged by --json, so both signals stay available.

How fast, and when this is the wrong tool

Each call is one process launch: ≈3–5 ms on Linux, ≈20–25 ms on Windows. The model checking itself is microseconds, so at that rate you are timing fork, not delhi.

Fine for scripting, dataset generation and batch evaluation — a few thousand checks is seconds. Not fine inside a training loop that queries per step: at 20 ms a call, a million queries is six hours of process creation.

If that is your shape, two ways out. delhi gui serves /api/eval, /api/ask and /api/state over loopback HTTP, and one long-lived process answering many requests avoids the launch entirely — though it is built as a debugging UI, so treat that surface as unstable. Otherwise open an issue: real PyO3 bindings are the answer, and knowing which calls sit in your hot path is what would shape them.

The language

A .delhi file has a signature, an initial state, optional constraints, and actions.

types   { Actor - Object }          // a type hierarchy
objects { alice, bob - Actor }      // things, with types
agents  { alice, bob }              // which of them have minds
props   { h, d }                    // propositions

constants { adjacent(hall, study) } // optional, static
define    { … }                     // optional, named formulas
rules     { … }                     // optional, Horn clauses
initially { … }  or  state { … }    // required, one of the two
goal      { φ }                     // optional
invariants{ φ … }                   // optional
actions   { … }                     // required, may be empty

Initial state

Two forms. initially is declarative — state facts and attitudes, and the model is constructed and then verified against every line you wrote:

initially {
    h                    // a fact about the actual world
    ?[carol] h           // carol cannot tell
    B[carol] h           // but she leans that way
}

state writes the model out by hand, and is exactly what delhi show prints:

state {
  *w1 <- { h }          // `*` marks the actual world
   w0 <- { }
  carol: w0 < w1        // w1 is the more plausible
}

< and <= point toward the more plausible world; ~ relates two worlds both ways.

Definitions

Named formulas, expanded before anything is lowered — the semantics never learns they existed. Parameters substitute objects, and may stand where an agent name does:

define {
    blocked(?r)       = !lit(?r) | locked(?r)
    can_enter(?w, ?r) = !blocked(?r) & K[?w] !blocked(?r)
}

Usable anywhere a formula is. Definitions may call definitions; a cycle is rejected when the table is built rather than caught by a depth limit.

Two things are refused deliberately. A definition cannot be causesd or written as a world fact, since both need an atom the semantics can set. And parameters range over objects, not formulas — define f(?p) = K[a] ?p is a second-order macro and is not supported.

Rules

Horn clauses over constants, saturated to a least fixpoint at parse time:

constants { !adjacent(Room, Room)  adjacent(hall, study)  adjacent(study, attic) }
rules {
    reach(?x, ?y) :- adjacent(?x, ?y)
    reach(?x, ?z) :- adjacent(?x, ?y), reach(?y, ?z)
}

reach(hall, attic) folds to true like any other constant. Derived predicates never become propositions, so they cost no bit in any world.

Constants only, and that restriction is the interesting part. The fixpoint runs once, which is sound only because the constant table is static. A rule over a fluent would have an extension varying per world and per action, so computing it would mean either a fixpoint per world at evaluation or maintaining derived atoms through product update — the frame problem again. It is refused with a message rather than half-supported.

Bodies carry no negation, which keeps the program monotone so the least fixpoint exists; and every head variable must appear in the body, or the head would assert facts the body never justified.

Invariants

Claims that must hold in every state, not only the first:

invariants { !((B[a] p & B[b] !p) | (B[a] !p & B[b] p)) }

An initially entry that drives no construction is already an assertion about the start; an invariant is the same claim made about the whole run, which is usually what a domain constraint means.

Comments

// to end of line, /* … */ for blocks.

Operators

Six primitives and nine sugar forms. Every one works in eval, in ask patterns, in goal, in invariants, and at the prompt.

Primitives

Closed under !, &, |, and nested arbitrarily. C[*] takes all agents; C[a,b] takes a group.

Sugar

The disjunction is why these exist as operators. "Does Alice know whether the coin is heads?" is not K[alice] h and not !K[alice] h — it is the or of two knowledge claims, and writing it out every time is how mistakes get made.

The laws each obeys

delhi verifies these as frame properties rather than assuming them.

K is S5 — K[a] φ → φ (T, factivity), K[a] φ → K[a] K[a] φ (4), !K[a] φ → K[a] !K[a] φ (5).

B is KD45 — B[a] φ → !B[a] !φ (D, consistency), plus 4 and 5. Notably not T: an agent can believe something false. That is the entire point.

[] is factive — [][a] φ → φ.

Bridges — K[a] φ → B[a] φ, B[a] φ → K[a] B[a] φ, K[a] φ → [][a] φ.

Strength ordering

K[a] φ    ⟹    [][a] φ    ⟹    B[a] φ

Knowledge is strongest, then safe belief, then belief. Each step reads over fewer worlds, so each is easier to satisfy. Safe belief is the useful middle: it survives learning any true fact, where a mere belief can be overturned by one.

$ delhi eval examples/coin_lie.delhi -f "[][carol] h"    # true
$ delhi eval examples/coin_lie.delhi -f "K[carol] h"     # false

Carol's belief that the coin is heads is safe — stable under any true news — without being knowledge, because she has not actually established it.

Plausibility direction

u R[i] v means v is at least as plausible as u. Plausibility increases along the arrow, and in the surface syntax it increases to the right:

carol: w0 < w1        // w1 is the more plausible

Worth pinning down, because an inverted ordering is still a well-formed model. Nothing will complain, and every answer will be quietly backwards.

Command line

delhi check <FILE>                          parse, ground, and validate
delhi state <FILE> [-a ACTION]…             facts, and each agent's attitudes
delhi show  <FILE>                          the model itself, in explicit form
delhi eval  <FILE> [-a ACTION]… -f φ        evaluate one formula
delhi ask   <FILE> [-a ACTION]… -q π        enumerate what holds; `_` is the hole
delhi step  <FILE> -a <ACTION>…             apply actions in sequence
delhi dot   <FILE>                          Graphviz
delhi repl  <FILE>                          explore interactively
delhi gui   [DIR] [-p PORT]                 browser UI over a folder of .delhi files
delhi bench <FILE> [-n CYCLES] -a ACTION…   model growth and timing
delhi --version | --help

Flags

• -a ACTION… — apply a trace before answering. Takes any number of ground action names. Available on state, eval, ask, step and bench.
• -f FORMULA — the formula for eval.
• -q PATTERN — the pattern for ask; _ marks the hole.
• -d DEPTH — modal nesting depth for ask candidates. Default 0.
• --json — one JSON object on stdout, errors included. On check, state, eval and ask.

Exit codes

The 1 / 2 split is deliberate: 2 means the question was wrong, 1 means the answer was no. A script that conflates them turns a typo into a refutation.

Colour

On when stdout is a terminal, off otherwise — so delhi dot … | dot -Tpng stays byte-clean. NO_COLOR=1 forces it off, CLICOLOR_FORCE=1 forces it on through a pipe.

The REPL

$ delhi repl examples/coin_lie.delhi
> B[carol] h              a bare formula evaluates
> :do peek_c()            apply an action
> :undo                   drop the last
> :reset                  clear the trace
> :state                  the state view
> :ask B[alice] _         enumerate; `:ask 2 …` sets the depth
> :actions                what can be applied
> :help

The browser UI

delhi gui serves the current directory — your own folder of .delhi files, not the repository. The ten examples are compiled into the binary, so a fresh install still opens on something readable.

cd ~/my-domains && delhi gui        # or: delhi gui ~/my-domains -p 9000

Editor with syntax highlighting and clickable errors, an actions rail, a live state view, a model graph, and a console with command history. Every divider is draggable. It binds to loopback and has no authentication, because it is a debugging tool for the machine it runs on — do not expose it.

Related systems

Epistemic planning has two traditions pulling against each other. One starts from expressiveness — dynamic epistemic logic will represent anything, at the cost of the modeller hand-building event models and of undecidable plan existence. The other starts from tractability — restrict the representation until an off-the-shelf planner can be pointed at it.

Action languages sit in between: keep a semantics grounded in DEL, but let the modeller declare who observes what and derive the event models from that. delhi is in this third camp, and specifically implements mB — the branch of that lineage that swapped knowledge for belief.

Expressiveness

Machinery

What "mB+" means

The name is delhi's own. Buckingham's mB defines its object language with six clauses: atoms, negation, conjunction, knowledge, belief, and common knowledge. Safe belief and conditional belief are genuinely absent from it.

They are not new to the world, though — they are Baltag and Smets's operators, and mB's plausibility models already contain everything needed to evaluate them. delhi adds them to the query language rather than to the semantics, and calls the result mB+ to be clear about which parts came from where.

What else is delhi's own rather than inherited:

• The ask query system. Patterns with a repeated hole, enumerated over modal literals — the PDKB representation used as a search space rather than a state representation.
• Invariants, definitions and Horn rules as language features.
• The performance work. Hash-consed formulas, bitset models and relations, memoised entailment, canonical state keys, and contraction wired into every trace.
• ~R proved sound and a congruence, with its incompleteness measured rather than assumed.

Reading the comparison honestly

Two caveats worth stating.

The planner column is where delhi is behind. EFP 2.0 and PDKB are planning systems with years of optimisation; delhi is a model checker with the pieces for a planner sitting idle. If you need plans, not answers about states, they are the mature tools today.

"Limited" for mA* is not a criticism. mA* deliberately trades expressiveness for tractability, and the trade buys real planning performance. The table records what each system chose, not how well it did it.

Further reading

The primary sources for delhi

Buckingham, D. (2021). Epistemic Planning with Belief. PhD thesis. The direct source for mB — the plausibility-model semantics, the action types, the observability model, and the Coin Lie scenario that runs through delhi's examples and this book.

Buckingham, Wang & Sardiña (2021). "Epistemic Planning with Belief" and its companion paper at KR 2021. The conference-length presentations of the above.

Where belief revision comes from

Baltag, A. & Smets, S. (2006). "Conditional Doxastic Models: A Qualitative Approach to Dynamic Belief Revision." ENTCS 165. Plausibility models, safe belief, conditional belief — the operators delhi's [] and B^ψ implement.

Baltag, A. & Smets, S. (2008). "A Qualitative Theory of Dynamic Interactive Belief Revision." Texts in Logic and Games 3. The fuller treatment, including action-priority update.

Dynamic epistemic logic generally

van Ditmarsch, van der Hoek & Kooi (2007). Dynamic Epistemic Logic. Springer. The standard textbook. Start here if the logic chapters of this book left you wanting the full development.

Baltag, Moss & Solecki (1998). "The Logic of Public Announcements, Common Knowledge, and Private Suspicions." Where event models and product update come from — the machinery underneath How attitudes change.

Fagin, Halpern, Moses & Vardi (1995). Reasoning About Knowledge. MIT Press. The foundational text for the static side: possible worlds, S5, common knowledge, and the muddy children puzzle done properly.

Epistemic planning

Bolander & Andersen (2011). "Epistemic Planning for Single- and Multi-Agent Systems." Establishes plan existence as undecidable in general DEL — the result the action languages exist to route around.

Baral, Gelfond, Pontelli & Son. The mA* line of work: an action language for epistemic planning that trades expressiveness for tractability.

Le, Fabiano, Son & Pontelli (2018). "EFP and PG-EFP: Epistemic Forward Search Planners in Multi-Agent Domains," and Fabiano et al.'s EFP 2.0. The performance benchmark for forward-search epistemic planning.

Muise, Belle, Felli, McIlraith, Miller, Pearce & Sonenberg. The PDKB line — proper epistemic knowledge bases, depth-bounded, compiled to classical planning. delhi borrows the modal-literal representation for its ask enumeration.

Theory of mind, empirically

The false-belief tasks delhi's examples reproduce come from developmental psychology rather than logic:

Wimmer & Perner (1983). "Beliefs about beliefs" — the original false-belief paradigm.

Baron-Cohen, Leslie & Frith (1985). "Does the autistic child have a 'theory of mind'?" The Sally-Anne task as it is now known.

Sullivan, Zaitchik & Tager-Flusberg (1994). "Preschoolers can attribute second-order beliefs." The Birthday Bicycle Story — examples/bicycle.delhi.

Perner & Wimmer (1985). "'John thinks that Mary thinks that…'" Second-order attribution and the ice-cream van task — examples/ice_cream_van.delhi.