The Leanpub 60 Day 100% Happiness Guarantee
Within 60 days of purchase you can get a 100% refund on any Leanpub purchase, in two clicks.
See full terms...
Automated Reasoning: Logic, AI Agents and LLMs
Master Logic, Search, SAT/SMT, Theorem Proving, Verification and Neuro-Symbolic AI
What You Will Learn
A conceptual journey from Logic and Search to Theorem Proving, Constraint Solving, Formal Verification, and the future of Neuro-Symbolic AI
Chapter 1. Automated Reasoning and Machine Learning
Understand the fundamental differences between learning from data and reasoning from explicit knowledge and rules — and why modern AI increasingly needs both.
Chapter 2. Automated Reasoning and Generative AI, LLMs
Explore the limitations of purely generative systems and understand where Automated Reasoning can complement LLMs.
Chapter 3. Logic, First-Order Logic, Predicate Logic
Understand the foundations of symbolic reasoning and how logic allows knowledge and relationships to be represented in a form machines can reason about.
Chapter 4. Knowledge Representation, Inference and Proof Systems
Learn how machines represent knowledge, derive new conclusions, and establish whether a conclusion follows from known facts and rules.
Chapter 5. Search, Constraint Satisfaction Problems and Planning
Understand reasoning as a search problem and see how constraints reduce the space of possible solutions.
Chapter 6. Automated Planning and Decision Making
Explore how AI can reason about actions, consequences, goals, and possible future states in order to choose what to do.
Chapter 7. Automated Theorem Proving, Resolution and Unification
Understand how machines can automatically construct logical proofs and why techniques such as resolution and unification are fundamental to this process.
Chapter 8. Proof Search and Theorem Provers
Explore proof construction as a search problem and understand how theorem provers navigate enormous spaces of possible reasoning paths.
Chapter 9. Constraint Programming
Understand how problems can be expressed through variables, domains, and constraints, allowing machines to search for valid solutions systematically.
Chapter 10. Optimization and Scheduling
See how reasoning and constraint solving can be used to find not merely valid solutions, but better solutions under competing objectives.
Chapter 11. Search Algorithms
Understand the fundamental search strategies that allow machines to navigate large spaces of possible states, solutions, and reasoning paths.
Chapter 12. SAT Solvers, SMT Solvers and Decision Procedures
Understand why SAT and SMT solvers have become powerful general-purpose reasoning engines and how they can automatically determine whether complex logical constraints are satisfiable.
Chapter 13. Constraint Solving and Symbolic Execution
Explore how programs can be analyzed symbolically rather than executed only with concrete inputs, enabling machines to reason about many possible executions.
Chapter 14. Formal Verification
Understand the fundamental idea behind formally proving that a system satisfies its specification instead of relying only on testing.
Chapter 15. Program Verification
Explore how Automated Reasoning can be used to establish properties such as program correctness, safety, and the absence of certain classes of errors.
Chapter 16. Hardware Verification
Understand how formal methods and automated reasoning are used to verify extremely complex hardware systems where traditional testing alone is insufficient.
Chapter 17. Model Checking
Learn how systems can be automatically explored to determine whether they satisfy specified properties — and how counterexamples can reveal incorrect behavior.
Chapter 18. Proof of Correctness
Understand what it actually means to prove that a program or system is correct and how mathematical reasoning becomes an engineering tool.
Chapter 19. Symbolic Verification
Explore how symbolic representations allow verification systems to reason about enormous numbers of possible states without explicitly enumerating every one.
Chapter 20. Case Study — How Does Intel Verify CPUs?
See how Automated Reasoning and Formal Verification are applied to one of the most complex engineering problems in computing: verifying modern processors.
Chapter 21. Case Study — How Does NASA Verify Spacecraft Software?
Discover how formal methods and rigorous reasoning help verify software for systems where failures can have extraordinary consequences.
Minimum price
$24.99
$34.99
You pay
Author earns
PDF
About
About the Book
Generative AI has become remarkably good at understanding language, generating content, and solving increasingly complex problems. But there is a fundamental limitation: generating a plausible answer is not the same as reasoning with certainty. This is where Automated Reasoning becomes increasingly important.
From LLMs and Generative AI to AI Agents and Neuro-Symbolic AI, the next generation of intelligent systems needs more than neural networks alone. It needs the ability to represent knowledge explicitly, search through possible solutions, enforce constraints, verify conclusions, prove correctness, and make decisions according to well-defined rules. Automated Reasoning provides many of these capabilities.
This book takes you on a journey from Logic, Knowledge Representation, Search, Constraints, and Planning to Theorem Proving, SAT/SMT Solving, Symbolic Execution, and Formal Verification — and finally connects these ideas to real-world systems such as CPU verification at Intel and spacecraft software verification at NASA.
You will not learn Automated Reasoning as a collection of complicated mathematical formulas or isolated algorithms. Instead, you will learn to understand why these technologies exist, what problems they were created to solve, how they fit together, and why they are becoming increasingly relevant to Generative AI, AI Agents, and the emerging Neuro-Symbolic AI paradigm.
Understand the Reasoning Behind AI — Not Just the Algorithms
Much of modern AI is built around neural networks. LLMs can learn patterns from enormous amounts of data and generate remarkably sophisticated responses. However, neural generation has an important limitation: an answer can be convincing without necessarily being guaranteed to be correct.
This creates a fundamental question: What happens when AI needs to do more than generate — when it needs to reason, plan, verify, and act reliably?
Automated Reasoning offers a different perspective. Instead of asking only “What answer is likely?”, we can ask:
What knowledge do we have?
What rules must hold?
What possibilities are allowed?
What constraints must be satisfied?
Can this conclusion be proven?
Can this program be guaranteed to behave correctly?
These ideas have existed for decades in logic, theorem proving, constraint solving, planning, and formal verification. What is changing today is their relationship with modern neural AI.
The emerging Neuro-Symbolic AI paradigm seeks to combine the strengths of both worlds:
- Neural AI provides perception, language understanding, learning, and flexible generation.
- Symbolic AI and Automated Reasoning provide explicit knowledge, structured reasoning, constraints, search, planning, and verification.
The result is not simply a larger language model. It is a different way of thinking about intelligent systems: neural models generate possibilities; symbolic systems can constrain, reason about, search through, and verify those possibilities.
This book is designed for people who want to understand that bigger picture.
You will focus on the ideas and principles behind the technology, rather than getting lost in mathematical notation or implementation details. For every major concept, the goal is to answer three fundamental questions: Why does it exist? What problem does it solve? How does it work at a conceptual level?
By the end of the book, you should be able to see Automated Reasoning not as an old and isolated branch of AI, but as one of the foundations that may become increasingly important as AI evolves from systems that generate answers toward systems that reason, plan, verify, and take actions.
Author
About the Author
T.N.K.TECH
I write about Artificial Intelligence, software engineering, and emerging technologies with a focus on making complex technical ideas easier to understand.
My work explores the foundations behind modern AI, including Automated Reasoning, Reasoning Models, AI Agents, Neuro-Symbolic AI, Formal Verification, and trustworthy intelligent systems.
I am particularly interested in explaining not only how a technology works, but also why it exists, what problem it solves, and where it fits within the larger evolution of Artificial Intelligence.
Through books and educational content, my goal is to help readers build a deeper conceptual understanding of rapidly evolving technologies without getting lost in unnecessary complexity.
Earn $8 on a $10 Purchase, and $16 on a $20 Purchase
We pay 80% royalties on purchases of $7.99 or more, and 80% royalties minus a 50 cent flat fee on purchases between $0.99 and $7.98. You earn $8 on a $10 sale, and $16 on a $20 sale. So, if we sell 5000 non-refunded copies of your book for $20, you'll earn $80,000.
(Yes, some authors have already earned much more than that on Leanpub.)
In fact, authors have earned over $15 million writing, publishing and selling on Leanpub.
Learn more about writing on Leanpub
Free Updates. DRM Free.
If you buy a Leanpub book, you get free updates for as long as the author updates the book! Many authors use Leanpub to publish their books in-progress, while they are writing them. All readers get free updates, regardless of when they bought the book or how much they paid (including free).
Most Leanpub books are available in PDF (for computers) and EPUB (for phones, tablets and Kindle). The formats that a book includes are shown at the top right corner of this page.
Finally, Leanpub books don't have any DRM copy-protection nonsense, so you can easily read them on any supported device.
Learn more about Leanpub's ebook formats and where to read them
Write and Publish on Leanpub
You can use Leanpub to easily write, publish and sell in-progress and completed ebooks and online courses!
Leanpub is a powerful platform for serious authors, combining a simple, elegant writing and publishing workflow with a store focused on selling in-progress ebooks.
Leanpub is a magical typewriter for authors: just write in plain text, and to publish your ebook, just click a button. (Or, if you are producing your ebook your own way, you can even upload your own PDF and/or EPUB files and then publish with one click!) It really is that easy.