Your agent's LLM is fluent, and sometimes it is wrong and sure. It "remembers" Anna and Lena meeting in Berlin while its own memory has Anna in Lisbon at the same hour. A prompt cannot tell that guess from a fact. A logic layer can, and it can say why. The LLM proposes. The logic decides.
This book teaches that logic from zero, the way The Little Schemer taught recursion: one question at a time. Most pages are short question-and-answer frames: cover the answer, think, then look. Fifteen Laws of Logic Agents sum up what the frames earn, from "A fact is a rule that needs nothing. A rule is a fact that waits." to "An agent that cannot say 'no' cannot be trusted with 'yes'."
The destination is higher-order logic programming in λProlog. The last book-length introduction to it, Dale Miller and Gopalan Nadathur's Programming with Higher-Order Logic (2012), is excellent and academic. Agents changed who needs it: typed predicates, binders, scoped assumptions, and rules about rules are what the logic layer of a neurosymbolic agent is made of. Here they run in lean-elpi, an implementation of the ELPI dialect of λProlog inside Lean 4, usable from the command line and Python.
What you will learn and build
- Part I, The Little Logician. What neurosymbolic AI is and where logic sits in an agent. First-order logic through facts, rules, and questions. Prolog and Datalog in a nutshell: unification, backtracking, search trees, negation as failure, and why Datalog always finishes.
- Part II, The Seasoned Logician. λProlog with lean-elpi: types and modes that refuse an ill-formed fact before it loads; predicates as values; lambdas and binders, so queries become data the agent can store and pass;
pi and => for what-if questions that leave memory untouched; meta-interpreters that print a proof as an explanation; and constraint handling rules for goals that wait for information. - Part III, The Logic Layer. LF proof certificates checked by Lean's kernel. The logic layer in Python: propose, check, commit. An LLM that writes λProlog, guarded by the parser, the type checker, the mode checker, a fuel limit, and a consistency check. And a complete little agent that refuses the phantom, explains why, answers a what-if, and lets a rule call the LLM back, with the answer still checked.
Every chapter also says what its technique does not give you. A logic layer checks a fact against your rules. It cannot make a consistent invention true.
Who it is for
AI and agent engineers who know Python and LLMs and have never seen Prolog, logic notation, or the λ-calculus. No mathematics background is assumed: every idea arrives as code you can run, then a picture, then notation. Bulletproof Knowledge, the author's book on proofs in Lean, is a companion, not a prerequisite.
What you get
- 13 short chapters in three parts, about 330 print pages, 22 diagrams
- Hundreds of question-and-answer frames and the fifteen Laws, collected on one page
- Exercises graded ★ to ★★★ in every chapter from Chapter 2, with tested solutions
- λProlog at a Glance (a two-page cheat sheet), a glossary, and a bibliography
- The Apache-2.0 companion code at github.com/Volland/logic-for-agents, where CI runs every example and solution on lean-elpi v0.4. The agent uses the Anthropic SDK and replays recorded responses by default, so you need no API key.
