369. Let Ci = (l ∨αi) and 
. Each omitted clause 
, where 1 < i ≤ p and r < j ≤ q, is redundant, because it is a consequence of the non-omitted clauses 
, (l1 ∨ . . . ∨ lr ∨ βj) via hyperresolution. [This technique is called “substitution,” because we essentially replace |l| by its definition.]
370. 
. (See the discussion following 7.1.1–(27). In general, ...
Get The Art of Computer Programming: Satisfiability, Volume 4, Fascicle 6 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.
