Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).
5.4 Proving by Contradictions
Definite clauses can be used in a proof by contradiction by allowing rules that give contradictions. For example, in the electrical wiring domain, it is useful to be able to specify that some prediction, such as light l2 is on, is not true. This will enable diagnostic reasoning to deduce that some switches, lights, or circuit breakers are broken.
