Logical and Compositional Foundations of AI: Proof, Semantics, Composition, and Verifiable Machine Reasoning

How can an AI system produce answers, programs, plans, and tool calls that remain trustworthy even when the learned model itself is not? This volume develops the mathematical foundations for answering that question through proofs, certificates, semantics, interfaces, and compositional guarantees.

Beginning with propositional and first-order logic, computability, type theory, and proof assistants, the book builds a rigorous path through SAT and SMT certificates, program semantics and logics, temporal logic and model checking, abstract interpretation, categorical and monoidal composition, contracts, effects, information flow, proof search, program synthesis, and formal verification of learned components. The final chapters bring these tools together in architectures for verified agents and proof-carrying AI.

Throughout, the emphasis is not merely on whether a component can be verified, but on exactly what is guaranteed, under which quantifiers and assumptions, and relative to which trusted base. A recurring AgentDSL example connects the mathematics to modern large-model systems involving structured generation, tools, memory, learned guards, runtime monitors, and shields.

Written for graduate students, researchers, and technically advanced practitioners, the book provides a unified framework for moving from untrusted generators to checkable evidence and from local component guarantees to system-level assurance.