CHAPTER 4RESOLUTION
In Chapter 3, we examined how FOL could be used to represent knowledge about a simple application domain. We also showed how logical reasoning could be used to discover facts that were only implicit in a given knowledge base. All of our deductive reasoning, however, was done by hand, and relatively informally. In this chapter, we will examine in detail how to automate a deductive reasoning procedure.
At the knowledge level, the specification for an idealized deductive procedure is clear: Given a knowledge base KB and a sentence α, we would like a procedure that can determine whether or not KB 
α also, if β[x1,…, xn] is a formula ...
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.
