14
Resolution in the Propositional Calculus
14.1 A New Rule of Inference: Resolution
14.1.1 Clauses as wffs
In the last chapter, I mentioned several rules of inference, including modus ponens. Many of these can be combined into one rule, called resolution. The version of resolution that I will use in this book applies to a special format for wffs called clauses, which I now define.
First, recall that a literal is either an atom (in which case, it is called a positive literal) or the negation of an atom (in which case, it is called a negative literal). A clause is a set of literals. The set is an abbreviation for the disjunction of all the literals in the set. Thus, a clause is a special kind of wff. I usually write clauses as disjunctions, but some ...
Get Artificial Intelligence 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.
