April 1998
Beginner
513 pages
14h 32m
English
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 ...
Read now
Unlock full access