Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).
5.2.2 Proofs
So far, we have specified what an answer is, but
not how it can be computed. The definition of 
specifies
what propositions should be logical consequences of a knowledge base but not how to compute
them. The problem of deduction is
to determine if some proposition is a logical consequence of a
knowledge base. Deduction is a specific form of inference.
A proof is a mechanically derivable demonstration that a proposition logically follows from a knowledge base. A theorem is a provable proposition. A proof procedure is a - possibly non-deterministic - algorithm for deriving consequences of a knowledge base. See the box for a description of non-deterministic choice.
Given a proof procedure, KB 
g means g can be
proved or derived
from knowledge base
KB.
A proof procedure's quality can be judged by whether it computes what it is meant to compute.
A proof procedure is sound with respect
to a semantics if everything that can be derived from a knowledge base
is a logical consequence of the knowledge base. That is, if
KB g, then KB g.
A proof procedure is complete with
respect to a semantics if there is a proof of each logical consequence
of the knowledge base. That is, if KB g, then KB g.
We present two ways to construct proofs for propositional definite clauses: a bottom-up procedure and a top-down procedure.
