CHAPTER 5REASONING WITH HORN CLAUSES
In Chapter 4, we saw how a Resolution procedure could in principle be used to calculate entailments of any first-order logic KB. But we also saw that in its most general form Resolution ran into serious computational difficulties. Although refinements to Resolution can help, the problem can never be completely eliminated. This is a consequence of the fundamental computational intractability of first-order entailment.
In this chapter, we will explore the idea of limiting ourselves to only a certain interesting subset of first-order logic, where the Resolution procedure becomes much more manageable. We will also see that from a representation standpoint, the subset in question is still sufficiently expressive ...
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.
