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 that light $l_2$ is on, is not true. This will enable diagnostic reasoning to deduce that some switches, lights, or circuit breakers are broken.