(9th-August-2020)
• 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.
Horn Clauses
Assumables and Conflicts
Consistency-Based Diagnosis
Reasoning with Assumptions and Horn Clauses
Bottom-Up Implementation
Top-Down Implementation
The definite clause language does not allow a contradiction to be stated. However, a simple expansion of the language can allow proof by contradiction.
An integrity constraint is a clause of the form
false←a1∧...∧ak.
where the ai are atoms and false is a special atom that is false in all interpretations.
A Horn clause is either a definite clause or an integrity constraint. That is, a Horn clause has either false or a normal atom as its head.
Integrity constraints allow the system to prove that some conjunction of atoms is false in all models of a knowledge base - that is, to prove disjunctions of negations of atoms. Recall that ¬p is the negation of p, which is true in an interpretation when p is false in that interpretation, and p∨q is the disjunction of p and q, which is true in an interpretation if p is true or q is true or both are true in the interpretation. The integrity constraint false←a1∧...∧ak is logically equivalent to ¬a1∨...∨¬ak.
A Horn clause knowledge base can imply negations of atoms, as shown in Example 5.16.
Comments