An assistant agent keeps a memory of the people, places and meetings in its user’s life. Its calendar says that on Tuesday, from ten to noon, Anna is at the project kickoff in Lisbon.

Then the agent reads a chat log, and its language model proposes a new memory: Anna and Lena met in Berlin on Tuesday, from ten to noon.

The sentence is fluent. The names are right, the city is real, the time is plausible. The model is sure. And it is wrong: Lisbon and Berlin are about 2,300 kilometers apart, and no meeting room is that large.

A person catches this in a second. Most agents don’t.

Why this matters more for agents than for chat

In a chat, a hallucination costs one bad answer. You read it, you frown, you move on.

An agent with a memory is different. It stores the mistake. Then it reasons from it. Tomorrow it tells you that Anna and Lena know each other well, that Lena’s team works with Anna’s, that a follow-up in Berlin makes sense. Each new conclusion sounds as sure as the first, and each one is built on a meeting that never happened.

The usual tools don’t help:

  • A better prompt asks the model to be careful. It can’t make the model know what it doesn’t know.

  • A vector store finds notes that look similar. Lisbon and Berlin are both cities in the same week; retrieval happily returns both, and can’t say which one is true.

  • A second model as judge produces a verdict that is plausible, not one that is right. It is another guess, in the same confident voice.

What’s missing is a part of the agent that can tell a guess from a fact, and say why.

We have been here before

That part is older than deep learning. In the 1970s and 80s, expert systems such as MYCIN and XCON kept knowledge as rules. They applied the same rule the same way every time. When you asked “why?”, they showed you the chain of rules that led to the answer.

They failed at one thing: getting knowledge in. Every fact and every rule was typed by hand, by experts, at great cost. That bottleneck, not the logic, is what sank them.

Large language models are very good at exactly that one thing. They read chat logs, emails and documents, and turn them into candidate facts at almost no cost.

So the two halves of AI fit together. This is what neurosymbolic AI means in practice:

The LLM proposes. The logic decides.

That is the First Law of the book, and the pattern behind everything else in it. The model guesses; a small logic layer checks the guess against what the agent already knows and the rules it lives by; only then does the agent commit it to memory. The book calls this the propose, check, commit loop.

What the fix looks like

Here is the whole rule that catches the phantom meeting. It is λProlog, and it is the first rule the book asks you to read:

% Nobody can be in two places at once.
bilocated P C1 C2 :-
  proposed _ K1 W1 C1 S1 E1, physical K1, std.mem W1 P,
  event _ K2 W2 C2 S2 E2,    physical K2, std.mem W2 P,
  not (C1 = C2),
  overlaps S1 E1 S2 E2.

Read it aloud: Person P is in two places at once if a proposed event puts P in city C1, a stored event puts P in city C2, both events are physical, the cities differ, and the times overlap.

Run it, and it answers:

anna in berlin and lisbon

The rule does not care how sure the model sounded. It has no input for that. It gives the same answer every time, you can read it, test it, and fix it. And when it refuses a memory, it can print the reason: the rule it broke and the two events that clash.

“Why not just write an if in Python?”

For one rule, do. The trouble starts at twenty. Rules call each other. Chains of “reports to” need recursion. Every answer needs a reason. And sooner or later you want the LLM to propose a rule, not just a fact, and to check that rule before you run it.

Hand-written checks give you none of that. You end up writing a small, untyped rule engine. A rule engine with types is what λProlog already is.

And this is why the book goes past Prolog and Datalog to higher-order logic programming. Agents need things first-order rules don’t give you:

  • Types that refuse an ill-formed fact before it loads. A person can never stand where a city is expected.

  • What-if questions that leave memory untouched. => adds an assumption for one question only; when the question is answered, the memory is exactly as it was.

  • Rules as data, so the LLM can write new rules, and the logic can check them.

  • Explanations printed from proofs, every step tagged with where it came from.

  • Proofs a small kernel can check, so you trust the checker, not the search that found the answer.

In the last part of the book, the LLM writes λProlog itself. Everything it writes passes six guards in order: parse, type check, mode check, allowed predicates, a sandboxed run with a fuel limit, and a consistency check. A failed guard’s message goes back to the model so it can try again.

What it does not fix

I want to be honest about this, because the book is.

Logic checks a fact against your rules. It cannot check it against the world. If the model invents something that fits every rule, it gets in. On the book’s labelled test set, the logic layer stopped four of the six false proposals and lost two of the four true ones. A stricter rule catches more lies and loses more truths.

Logic won’t save you from rules nobody wrote, or rules that are wrong. What it gives you is a part of the agent that is wrong the same way every time, that you can read, and that can say no. That’s the Fifteenth Law, the one I’d keep if I could keep only one:

An agent that cannot say “no” cannot be trusted with “yes”.

Why I wrote a Little book

Here is the real problem. The ideas above are decades old and well understood. But the last book-length introduction to higher-order logic programming, Miller and Nadathur’s Programming with Higher-Order Logic (2012), is excellent and written for researchers. Most agent engineers will never open it.

So I wrote this one the way The Little Schemer taught recursion: short questions on the left, short answers on the right, one idea at a time. Here is how Chapter 1 reads, right after the rule catches the phantom:

Who decided the three verdicts? The rules. The LLM proposed all three in the same confident voice. The logic sorted them.
Did the logic care how sure the LLM sounded? No. It has no input for that.

Every idea arrives as code you run first, then a picture, then notation. No background in logic or mathematics is assumed. If you know Python and you’ve built something with an LLM, you can start on page one.

What’s inside

Part I: The Little Logician. Neurosymbolic AI, gently. Facts, rules and questions. Prolog and Datalog in a nutshell, and why “Datalog always finishes; Prolog only promises to try.”

Part II: The Seasoned Logician. Higher-order logic programming in λProlog with lean-elpi: types and modes, predicates as values, lambdas and binders, pi and => for what-if reasoning, rules about rules, meta-interpreters that explain, and constraints that wait.

Part III: The Logic Layer. Proof certificates that Lean’s kernel checks. The logic layer of an agent in Python. An LLM that writes λProlog behind the guards. And a complete little agent that refuses the phantom, explains its answers, and answers what-ifs without touching its memory.

Thirteen chapters, about 330 pages, fifteen Laws of Logic Agents, and exercises with tested solutions. Every example runs in CI, and the agent replays recorded LLM sessions, so you don’t need an API key to follow along.

Get the book

Logic for Agents: Building Neurosymbolic AI with Elpi is out now, complete.

If you want the deeper version, where every fact in memory carries a proof in Lean 4, Bulletproof Knowledge is the sibling book in the same Neurosymbolic AI series, and Leanpub has the two as a bundle.

Let the LLM guess. Let logic decide what your agent remembers, and make it say why.

If you know an engineer whose agent remembers things that never happened, forward this to them.