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, ...
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Read now
Unlock full access