(28th-July-2020)
• 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.
•
• The first proof procedure is a bottom-up proof procedure to derive logical consequences. It is called bottom-up as an analogy to building a house, where we build on top of the structure we already have. The bottom-up proof procedure builds on atoms that have already been established. It should be contrasted with a top-down approach, which starts from a query and tries to find definite clauses that support the query. Sometimes we say that a bottom-up procedure is forward chaining on the definite clauses, in the sense of going forward from what is known rather than going backward from the query.
• The general idea is based on one rule of derivation, a generalized form of the rule of inference called modus ponens:
• If "h←b1∧...∧bm" is a definite clause in the knowledge base, and each bi has been derived, then h can be derived.
• This rule also covers the case when m=0; the bottom-up proof procedure can always immediately derive the atom at the head of a definite clause with no body.
Comments