CHAPTER 6PROCEDURAL CONTROL OF REASONING
Theorem-proving methods, like Resolution, are general, domain-independent ways of reasoning. A user can express facts in full FOL without having to know how this knowledge will ultimately be used for inference by an automated theorem-proving (ATP) procedure. The ATP mechanism will try all logically permissible uses of everything in the knowledge base in looking for an answer to a query.
This is a double-edged sword, however. Sometimes, it is not computationally feasible to try all logically possible ways of using what is known. Furthermore, we often do have an idea about how knowledge should be used or how to go about searching for a derivation. When we understand the structure of a domain or a problem, ...
Get Knowledge Representation and Reasoning now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
