The following are the main points you should have learned from this chapter:

• •

  Representing constraints in terms of propositions often enables constraint reasoning to be more efficient.

• •

  A definite-clause knowledge base can be used to specify atomic clauses and rules about a domain when there is no uncertainty or ambiguity.

• •

  Given a set of statements that are claimed to be true about a domain, the logical consequences characterize what else must be true.

• •

  A sound and complete proof procedure can be used to determine the logical consequences of a knowledge base.

• •

  Bottom-up and top-down proof procedures can be proven to be sound and complete.

• •

  Proof by contradiction can be used to make inference from a Horn clause knowledge base.

• •

  Negation as failure can be used to make conclusions assuming complete knowledge.

• •

  Abduction can be used to explain observations.

• •

  Consistency-based diagnosis and abductive diagnosis are alternative methods for troubleshooting systems.

• •

  A causal model predicts the effect of interventions.

• •

  SAT solvers play a critical role in many important applications.