An agent with a memory has a new way to be wrong. A chatbot that hallucinates says something false once. An agent that hallucinates into its memory says it again tomorrow, builds on it, and answers every later question on top of a contradiction nothing in the pipeline noticed. Retrieval cannot tell which of two contradictory notes is right, and asking a second model "is this consistent?" only moves the hallucination from the fact to the verdict.

This book builds the missing piece: a small, fixed checker that decides what an agent may remember and what it may claim. A fact enters memory only with a proof that the memory stays consistent, and an answer leaves it only with a proof from what is stored. The agent's ontology of people, places, organizations and events is written as types in Lean 4, its rules about the world as propositions, and every accepted fact carries a certificate checked by Lean's kernel. Rules and search come from λProlog, running inside Lean through lean-elpi, and when a search finds an answer, the kernel checks that too. The LLM proposes, Lean decides, and a rejection goes back to the model with the name of the broken rule.

The promise is narrow on purpose. A checker guarantees consistency with your axioms, not truth about the world, and every chapter says what its technique does not give you. You do not need to know Lean, Prolog, dependent types or formal logic, and you do not need to be deep in mathematics: both languages are taught from zero, with code first, then a picture, then notation. Every snippet is cut from a public repository that compiles, and every output and error message in the book is the one Lean actually prints.

What you will build

• A typed ontology for agent memory in which an ill-typed fact does not compile
• A certified store whose insert returns a new store with a new proof, or names the axiom that blocks the fact
• Hierarchies of places and events with type classes, subtypes and coercions
• Proofs about the ontology itself: invariants, safe updates and schema migrations
• Rules over the memory in λProlog, hypothetical questions that leave no trace, and search results turned into kernel-checked certificates
• An agent, written entirely in Lean, that turns away six kinds of hallucination, feeds each rejection back to the LLM, and answers only with certificates

Who it is for

Engineers who build AI agents: you know Python, you have built with LLMs, and you know roughly what RAG and a knowledge graph are. Logicians and type theorists will find familiar ideas applied to an unfamiliar problem, with reading lists to the deeper sources.

What you get

12 chapters in three parts, 33 diagrams, exercises with compiled solutions, a 60-term glossary, and the Apache-2.0 companion code at github.com/Volland/bulletproof-knowledge: Lean 4 v4.35.0 and lean-elpi v0.3.3, no Mathlib, one lake build.

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.

What eats a fly? Ask the pond.

A small pond: algae, snails and flies, frogs and fish, a duck, a heron and an otter. Eleven short lines say who eats whom. Type a question, eats X fly, and a program answers: the frog, then the fish. It does not search the web or guess. It answers only from what the lines say, and it tells you when they say nothing.

That is a logic program: a list of things that are true, and a way to ask what follows. This little book teaches the idea from zero, in the question-and-answer style of The Little Schemer. Each page is two columns, a short question on the left and a short answer on the right. Cover the answers with a card, try, then look. Now and then a box states a Maxim, a short rule the questions above it have earned, from "A fact says what is true. A question asks whether it follows." to "A typing rule is a clause. A type checker is a logic program, and it runs both ways."

The language is λProlog, a younger and stranger relative of Prolog. It adds three things: types, so the computer turns away nonsense before it runs; predicates you pass around like numbers; and two small words, pi and =>, that let a program say "for any new thing" and "suppose this were true". Those three additions are what higher-order logic programming means. With them, a type checker for a little programming language fits in seven short clauses, and the same seven clauses infer types they were never told. That is where the book ends.

What you will learn

1. Facts and Questions. Constants, predicates, capital letters as holes, and what "no" really means.
2. Rules and Recursion. :- as "if", recursion that knows when to stop, and the search tree behind every answer.
3. Terms and Unification. Numbers built as trees, and how the engine makes two terms the same, or fails.
4. Lists. One append, run three ways: join, check and split. A relation has no inputs and outputs until you ask it something.
5. Types. Kinds, types and modes, and a checker that reads the program before it runs.
6. Predicates as Values. One rule for "above", "upstream of" and "older than"; map, filter and fold.
7. Lambdas. Predicates without names, terms with holes, and binders that cannot be captured.
8. Pi and Implication. What-if questions about a pond that is not quite this one.
9. The Little Type Checker. Seven clauses that check the types of a little language and, asked with a hole, infer them.

Who it is for

Students and programmers who have never taken a logic course. You need some programming in any language, a pencil, and patience. No mathematics, no Prolog and no Lean are assumed. You do not need to know what ∀ means; by Chapter 8 you will have written it. A chapter is an evening's work.

What you get

• 9 short chapters, 541 questions with their answers, and 11 Maxims collected on one page
• 35 exercises graded ★ to ★★★, each with a solution that runs
• 14 diagrams: the food web, search trees, term trees, and binders
• A two-page cheat sheet and a guided "Where to Go Next"
• The Apache-2.0 companion code at github.com/Volland/little-elpier: every program in the book, with every printed output kept as a golden file that a test checks

Every example runs

The engine is lean-elpi, an implementation of the ELPI dialect of λProlog written in Lean 4. pip install leanelpi gives you the whole engine with nothing to compile, on macOS, Linux and Windows with WSL; a Docker image and a build from source work too. The book's site, volland.github.io/little-elpier, has a sample of the frames.

About This Book

This book explores the intersection of formal logic, type theory, and knowledge representation, arguing for a fundamental shift from traditional RDF/OWL-based approaches to type-theoretic foundations for knowledge graphs and AI systems.

Overview

We stand at a critical juncture in knowledge representation. While RDF and OWL have served as foundational technologies for the semantic web, their limitations become increasingly apparent as we build more sophisticated AI systems requiring complex reasoning, contextual knowledge, and formal guarantees. This book presents a comprehensive exploration of how dependent type theory, higher-order logic, and advanced programming language concepts can revolutionize knowledge representation.

Drawing parallels between Russell's Paradox in set theory and current limitations in knowledge graphs, we demonstrate why moving beyond first-order logic is not just beneficial but necessary for the next generation of AI systems. The book combines theoretical foundations with practical implementations, showing how languages like Twelf, Beluga, ELPI, and TypeDB point toward a more expressive and reliable future for knowledge representation.

Key Topics

Foundational Concepts

• Dependent Type Theory: Types that depend on values, enabling precise specification of data relationships and constraints
• Higher-Order Logic: Quantification over predicates and functions for meta-level reasoning
• Logical Frameworks: LF and contextual modal type theory as foundations for formal systems
• Unification Theory: From Prolog's first-order unification to higher-order pattern unification

Programming Languages and Systems

• Lambda Prolog and ELPI: Higher-order logic programming for knowledge representation
• Twelf: Logical framework for encoding deductive systems and ontologies
• Beluga: Programming with contextual types and first-class contexts
• F*: Functional programming with dependent types for verified software
• TypeDB: Polymorphic database design with concept modeling

Knowledge Representation Evolution

• Beyond RDF Triples: Moving from binary relations to hypergraphs and metagraphs
• Ontology Verification: Formal validation of consistency, satisfiability, and structural properties
• Context-Sensitive Knowledge: Representing knowledge that varies by time, location, or perspective
• Constraint Integration: Unifying ontology definition with data validation

Advanced Applications

• AI Memory Systems: Type-theoretic approaches to artificial agent memory
• Personal Knowledge Graphs: Scalable, privacy-preserving knowledge for edge AI
• Hypergraph Ontologies: Native representation of n-ary relationships
• Scientific Knowledge Modeling: Formal approaches to evolving scientific understanding

Chapter Topics

1. Introduction: The Problem We Have vs. The Problem We Understand
2. Russell's Paradox and Knowledge Representation
3. From Set Theory to Type Theory
4. First-Order Logic and Its Limitations
5. Higher-Order Logic for Knowledge Graphs
6. Dependent Types: A New Paradigm for Ontologies
7. Lambda Prolog and ELPI: Logic Programming Meets Types
8. Twelf for Hypergraph Ontology
9. Beluga: Programming with Contexts
10. F: Verified Knowledge Systems*
11. TypeDB: Polymorphic Databases for AI
12. Understanding Unification: From Prolog to Higher-Order Logic
13. Emergent Intelligence in AI Agents and Knowledge Graphs
14. Personal Knowledge Graphs and Edge AI
15. Implementation Strategies and Practical Considerations

Target Audience

This book is designed for:

• Researchers in knowledge representation, semantic web, and formal methods
• AI Engineers building systems that require sophisticated knowledge modeling
• Graduate Students in computer science, particularly those studying logic, type theory, or AI
• Software Architects designing knowledge-intensive applications
• Ontology Engineers seeking more expressive and reliable representation frameworks

Prerequisites

Readers should have familiarity with:

• Basic logic and set theory
• Functional programming concepts
• RDF/OWL and semantic web technologies
• Fundamental computer science theory

No prior experience with dependent types or proof assistants is required, though familiarity with these concepts will enhance understanding.

What Makes This Book Different

Unlike traditional treatments of knowledge representation that focus on extending existing technologies, this book advocates for a fundamental paradigm shift. It bridges the gap between theoretical computer science (type theory, formal logic) and practical AI engineering, showing how advanced programming language concepts can solve real-world knowledge representation challenges.

The book emphasizes working implementations and practical examples rather than purely theoretical discussions, demonstrating how these advanced concepts can be applied to build more reliable, expressive, and verifiable knowledge systems.