;;;; proof of completeness of ground resolution
;;;; Matt Wilding  April 1988
;;;; This proof script executes on Matt Kaufmann's interactive enhancement
;;;; to the Boyer-Moore system
;; This proof script is a proof of the completeness of ground resolution
;; using Bledsoe's excess literal technique.  The final theorem is:
;;      (implies
;;       (and
;;        (unsatisfiable x)
;;        (validclauses x))
;;       (finishedproof x (getproof x)))
;; The proof script is in several sections:
;; 1) definitions required for understanding the theorem
;; 2) definition of getproof (a function that is conjectured to return a valid
;;      resolution proof that ends in box)
;; 3) proof of theorem
;; Section 1 is, strictly speaking, the only section needed to understand what has
;; been proven.

Event: Start with the initial nqthm theory.

;; added by Matt Kaufmann just to make nqthm-1991 happy!

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 1: definitions of terms in theorem

Definition: subset (x, y) = if listp (x)

then if car (x) ∈ y then subset (cdr (x), y) else f endif

else t endif

Definition: set-equal (s1 , s2 ) = (subset (s1 , s2 ) ∧ subset (s2 , s1 ))

Definition: set-member (x, list) = if listp (list)

then if set-equal (x, car (list)) then t

else set-member (x, cdr (list)) endif else f endif

;;  define what it means to be a valid set of clauses
;;  (ex.  (validclauses '((a b) ((not a) (not b)) ((not a) b) (a (not b)))) = t)

Definition: validliteral (l) = ((litatom (l) ∧ (l ≠ nil))

∨ (listp (l) ∧ (car (l) = 'not) ∧ litatom (cadr (l)) ∧ (cadr (l) ≠ nil) ∧ (cddr (l) = nil)))

Definition: validclause (c) = if listp (c)

then validclause (cdr (c))

∧ validliteral (car (c)) ∧ (car (c) ∉ cdr (c))

else c = nil endif

Definition: validclauses (cs) = if listp (cs) then validclause (car (cs)) ∧ validclauses (cdr (cs))

else cs = nil endif

;; unsatisfiablility of a set of clauses

Definition: unsatwith (clause, cs, values) = if listp (clause)

then if (list ('not, car (clause)) ∈ values) ∨ (cadar (clause) ∈ values) then unsatwith (cdr (clause), cs, values) else unsatwith (cdr (clause), cs, values)

∧ if listp (cs)

then unsatwith (car (cs), cdr (cs), cons (car (clause), values))

else f endif endif

else t endif

Definition: unsatisfiable (cs) = if listp (cs) then unsatwith (car (cs), cdr (cs), nil)

else f endif

Definition: takeout (list, x) = if listp (list)

then if x = car (list) then takeout (cdr (list), x)

else cons (car (list), takeout (cdr (list), x)) endif else nil endif

;; resolvent is valid resolvent of p1 and p2 resolving on something in p1list

Definition: resolvent-help (resolvent, p1list, p1 , p2 ) = if listp (p1list)

then if list ('not, car (p1list)) ∈ p2

then subset (takeout (p1 , car (p1list))

∪ takeout (p2 , list ('not, car (p1list))), resolvent)

∨ resolvent-help (resolvent, cdr (p1list), p1 , p2 ) elseif cadar (p1list) ∈ p2 then subset (takeout (p1 , car (p1list))

∪ takeout (p2 , cadar (p1list)),

resolvent) ∨ resolvent-help (resolvent, cdr (p1list), p1 , p2 ) else resolvent-help (resolvent, cdr (p1list), p1 , p2 ) endif

else f endif

Definition: resolvent (r, p1 , p2 ) = resolvent-help (r, p1 , p1 , p2 )

;; a valid resolution proof for a set of axioms is a set of triples where
;;each line of the proof has a resolvent and two (axiomatic or derived) parents

Definition: validproof (axioms, proof ) = if listp (proof )

then set-member (cadar (proof ), axioms)

∧ set-member (caddar (proof ), axioms)

∧ resolvent (caar (proof ), cadar (proof ), caddar (proof )) ∧ validproof (cons (caar (proof ), axioms), cdr (proof ))

else t endif

;; the empty clause is in a set of clauses

Definition: box-in-axioms (axioms) = if listp (axioms)

then if listp (car (axioms)) then box-in-axioms (cdr (axioms))

else t endif else f endif

Definition: last-element (list) = if listp (list)

then if listp (cdr (list)) then last-element (cdr (list))

else car (list) endif else nil endif

;; proof is a finished proof of axioms if there are no axioms, if
;; there are no axioms (and therefore satisfiable), if axioms include box,
;; or if proof is valid and has as its last resolvent box.

Definition: finishedproof (axioms, proof ) = ((¬ listp (axioms))

∨ box-in-axioms (axioms)

∨ (validproof (axioms, proof ) ∧ (car (last-element (proof )) ≃ nil)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 2:  getproof function developement

Definition: length (list) = if listp (list) then 1 + length (cdr (list))

else 0 endif

Theorem: list-means-length-more-0 listp (x) → (0 < length (x))

Definition: takeout1 (list, x) = if listp (list)

then if x = car (list) then cdr (list)

else cons (car (list), takeout1 (cdr (list), x)) endif else nil endif

Definition: listofcars (list) = if listp (list) then cons (caar (list), listofcars (cdr (list)))

else nil endif

;; some really useful rewrite rules for sets

Theorem: membership-on-subsets ((e ∈ a) ∧ subset (a, b)) → (e ∈ b)

Theorem: equals-has-same-members set-equal (a, b) → ((e ∈ a) = (e ∈ b))

Theorem: subset-is-transitive (subset (x, y) ∧ subset (y, z)) → subset (x, z)

Theorem: subset-fact-1 subset (x, y) → subset (x, cons (a, y))

Theorem: set-equals-fact set-equal (x, y) → set-equal (cons (a, x), cons (a, y))

Theorem: subset-of-self subset (x, x)

Theorem: set-equal-self set-equal (x, x)

Theorem: member-is-setmember (a ∈ x) → set-member (a, x)

Theorem: setmember-is-setmember-of-superset (set-member (a, x) ∧ subset (x, y)) → set-member (a, y)

Theorem: takeout-fact1 subset (takeout (s, x), takeout (cons (a, s), x))

Theorem: subset-of-union-fact-1 subset (a ∪ b, c) = (subset (a, c) ∧ subset (b, c))

Theorem: takeout-fact2 (a ∉ x) → set-equal (takeout (x, a), x)

Theorem: stupid-lemma1 (l ∈ c) → (subset (cons (l, c), d) = subset (c, d))

Theorem: stupid-lemma2 (l ∈ d) → (subset (c, cons (l, d)) = subset (c, d))

Theorem: stupid-lemma3 (l ∈ c) → (set-member (cons (l, c), d) = set-member (c, d))

;; some useful oddball facts about append other things

Theorem: member-of-append-1 (a ∈ x) → (a ∈ append (x, y))

Theorem: is-last-element-means-member (listp (p) ∧ (car (last-element (p)) = x)) → (x ∈ listofcars (p))

Theorem: membership-of-append (a ∈ x) → (a ∈ append (y, x))

Theorem: subset-of-append subset (x, y) → subset (x, append (z, y))

Definition: first-non-unit (clauses) = if listp (clauses)

then if 1 < length (car (clauses)) then car (clauses) else first-non-unit (cdr (clauses)) endif

else nil endif

Theorem: first-non-unit-fact2 (length (first-non-unit (x)) = 1) = f

Definition: take-out-literal (cs, c) = if listp (cs)

then if c = car (cs) then cons (cdr (c), cdr (cs))

else cons (car (cs), take-out-literal (cdr (cs), c)) endif else nil endif

Definition: take-out-clause (cs, c) = if listp (cs)

then if c = car (cs) then cons (list (car (c)), cdr (cs))

else cons (car (cs), take-out-clause (cdr (cs), c)) endif else nil endif Theorem: subset-of-takeouts-fact (validclauses (x) ∧ (a ∈ x) ∧ (list (car (a)) ∈ y) ∧ subset (takeout1 (x, a), y)) → subset (take-out-clause (x, a), y)

Theorem: take-out-literal-communative-sort-of (a ∈ x) → set-equal (take-out-literal (cons (y, x), a), cons (y, take-out-literal (x, a)))

Theorem: take-out-literal-preserves-validclauseness ((¬ box-in-axioms (cs)) ∧ validclauses (cs)) → validclauses (take-out-literal (cs, x))

Theorem: take-out-clause-preserves-validclauseness ((¬ box-in-axioms (cs)) ∧ validclauses (cs)) → validclauses (take-out-clause (cs, x))

Definition: find-contradiction (cs) = if listp (cs)

then if length (car (cs)) = 1

then if list (list ('not, caar (cs))) ∈ cdr (cs) then list (nil, car (cs), list (list ('not, caar (cs)))) elseif list (cadaar (cs)) ∈ cdr (cs) then list (nil, car (cs), list (cadaar (cs))) else find-contradiction (cdr (cs)) endif

else list (nil, nil, nil) endif else nil endif

Definition: number-of-lits (cs) = if listp (cs) then length (car (cs)) + number-of-lits (cdr (cs))

else 0 endif

Definition: excess-literal (cs) = (number-of-lits (cs) − length (cs))

Theorem: first-non-unit-fact ((excess-literal (cs) ≄ 0) ∧ (¬ box-in-axioms (cs))) → ((1 < length (first-non-unit (cs))) = t)

Definition: adjust (proof , cs, l)

= if listp (proof )

then if set-member (cadar (proof ), cs)

then if set-member (caddar (proof ), cs) then cons (car (proof ),

adjust (cdr (proof ), cons (caar (proof ), cs), l))

else cons (list (add-to-set (l, caar (proof )), cadar (proof ), add-to-set (l, caddar (proof ))),

adjust (cdr (proof ), cons (add-to-set (l, caar (proof )), cs), l)) endif

elseif set-member (caddar (proof ), cs) then cons (list (add-to-set (l, caar (proof )),

add-to-set (l, cadar (proof )), caddar (proof )),

adjust (cdr (proof ), cons (add-to-set (l, caar (proof )), cs), l))

else cons (list (add-to-set (l, caar (proof )), add-to-set (l, cadar (proof )), add-to-set (l, caddar (proof ))),

adjust (cdr (proof ), cons (add-to-set (l, caar (proof )), cs), l)) endif

else nil endif

Theorem: adjust-is-listp-when listp (p) → listp (adjust (p, x, l))

Theorem: when-first-non-unit-gives-clause ((¬ box-in-axioms (cs)) ∧ (excess-literal (cs) ≄ 0)) → (first-non-unit (cs) ∈ cs)

Theorem: no-box-fact (¬ box-in-axioms (cs)) → (number-of-lits (cs) ≮ length (cs))

Theorem: excess-literal-in-terms-of-cdr (listp (cs) ∧ (¬ box-in-axioms (cs))) → (excess-literal (cs)

= ((length (car (cs)) + excess-literal (cdr (cs))) − 1))

Theorem: when-take-out-literal-does-something ((¬ box-in-axioms (cs)) ∧ (excess-literal (cs) ≄ 0)) → ((excess-literal (take-out-literal (cs, first-non-unit (cs)))

< excess-literal (cs))

= t)

Theorem: not-box-when-clause-taken ((¬ box-in-axioms (cs)) ∧ (1 < length (x))) → (¬ box-in-axioms (take-out-clause (cs, x)))

Theorem: no-box-zero-el-fact (listp (x) ∧ (¬ box-in-axioms (x)) ∧ (excess-literal (x) ≃ 0)) → (excess-literal (cdr (x)) ≃ 0)

Theorem: take-out-clause-fact ((¬ box-in-axioms (cs)) ∧ (1 < length (x)) ∧ (x ∈ cs)) → ((excess-literal (take-out-clause (cs, x)) < excess-literal (cs)) = t)

Theorem: when-take-out-clause-does-something ((¬ box-in-axioms (cs)) ∧ (excess-literal (cs) ≄ 0)) → ((excess-literal (take-out-clause (cs, first-non-unit (cs)))

< excess-literal (cs))

= t)

Definition: getproof (cs) = if box-in-axioms (cs) then nil

elseif excess-literal (cs) ≃ 0 then list (find-contradiction (cs)) elseif car (last-element (adjust (getproof (take-out-literal (cs,

first-non-unit (cs))),

cs,

car (first-non-unit (cs)))))

= nil then adjust (getproof (take-out-literal (cs, first-non-unit (cs))),

cs,

car (first-non-unit (cs))) else append (adjust (getproof (take-out-literal (cs,

first-non-unit (cs))),

cs,

car (first-non-unit (cs))), getproof (take-out-clause (cs, first-non-unit (cs)))) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 3. Proof of the completeness theorem

;; the format of a resolution proof (implicit in validproof but useful to make explicit

Definition: proof-form (p) = if listp (p) then validclause (caar (p))

∧ validclause (cadar (p)) ∧ validclause (caddar (p)) ∧ (cdddar (p) = nil) ∧ proof-form (cdr (p))

else p = nil endif

;; some useful facts about valid proofs

Theorem: validproof-on-subset (subset (x, y) ∧ validproof (x, p)) → validproof (y, p)

Theorem: validproof-clauses-commutative set-equal (x, y) → (validproof (x, p) = validproof (y, p))

;; A useful fact about unsatisfiable sets of clauses

Theorem: assignment-interchangeable (unsatwith (c, cs, z) ∧ set-equal (y, z)) → unsatwith (c, cs, y)

;; lemmas about preservation of unsatisfiablility of clauses with some of
;; the literals removed

Theorem: take-out-literal-helper unsatwith (clause, cs, v) → unsatwith (car (take-out-literal (cons (clause, cs), x)),

cdr (take-out-literal (cons (clause, cs), x)), v)

Theorem: without-literal-still-unsatisfiable (unsatisfiable (cs) ∧ listp (cs)) → unsatisfiable (take-out-literal (cs, x))

Theorem: unsat-stepper (listp (x) ∧ unsatwith (x, cs, v)) → unsatwith (list (car (x)), cs, v)

Theorem: take-out-clause-helper (listp (x) ∧ unsatwith (clause, cs, v)) → unsatwith (car (take-out-clause (cons (clause, cs), x)),

cdr (take-out-clause (cons (clause, cs), x)), v)

Theorem: when-unsatisfiable unsatwith (clause, cs, z) → unsatwith (clause, cs, cons (x, z))

Definition: unsat-induct (c, x, cs, v) = if listp (cs)

then if (x = cadr (car (c))) ∨ (x = list ('not, car (c))) then t

else unsat-induct (car (cs), x, cdr (cs), cons (car (c), v)) endif else t endif

;; useful facts about negations of literals

Theorem: reversible-nots-1 ((length (y) = 1) ∧ litatom (x) ∧ (x ≠ nil) ∧ validclause (y) ∧ (x = cadar (y))) → (list (list ('not, x)) = y)

Theorem: reversible-nots-2 ((length (y) = 1) ∧ listp (x) ∧ validclause (y) ∧ (x = list ('not, car (y)))) → (list (cadr (x)) = y)

;; useful definition of set of clauses with all unit clauses

Definition: allunits (x) = if listp (x) then (length (car (x)) = 1) ∧ allunits (cdr (x))

else t endif

Theorem: allunit-means allunits (x) → (¬ listp (cdar (x)))

Theorem: allunits-if ((¬ box-in-axioms (x)) ∧ (excess-literal (x) ≃ 0)) → allunits (x)

Theorem: unit-clause-fact (length (x) = 1) → (takeout (x, car (x)) = nil)

Theorem: restriction-list-commutative set-equal (z1 , z2 ) → (unsatwith (x, y, z1 ) = unsatwith (x, y, z2 ))

Theorem: unsat-ignore-first-helper ((litatom (x) → (list (list ('not, x)) ∉ cons (c, cs))) ∧ (listp (x) → (list (cadr (x)) ∉ cons (c, cs)))

∧ allunits (cons (c, cs)) ∧ validclause (list (x)) ∧ validclauses (cons (c, cs)) ∧ unsatwith (c, cs, cons (x, v))) → unsatwith (c, cs, v)

;; base case of main theorem - if all clauses unit then getproof finds a proof

Theorem: no-excess-literal-proof (validclauses (cs) ∧ (¬ box-in-axioms (cs)) ∧ (excess-literal (cs) ≃ 0) ∧ unsatisfiable (cs)) → finishedproof (cs, list (find-contradiction (cs)))

;; useful definition of "almost" valid proof.  p is validproof of cs except that
;; some clauses in proof are missing literal l

Definition: validproof-but-for-literal (cs, p, l) = if listp (p)

then (set-member (cadar (p), cs) ∨ set-member (add-to-set (l, cadar (p)), cs)) ∧ (set-member (caddar (p), cs)

∨ set-member (add-to-set (l, caddar (p)), cs)) ∧ resolvent (caar (p), cadar (p), caddar (p)) ∧ validproof-but-for-literal (cons (caar (p), cs), cdr (p), l)

else t endif

;; some facts about validproof-but-for-literal

Theorem: validproof-but-for-literal-clauses-commutative set-equal (x, y) → (validproof-but-for-literal (x, p, l)

= validproof-but-for-literal (y, p, l))

Definition: adding-literal-induct (cs, p) = if listp (p) then adding-literal-induct (cons (caar (p), cs), cdr (p))

else t endif

Theorem: adding-literal-fact validproof-but-for-literal (cons (x, cs), p, l) → validproof-but-for-literal (cons (add-to-set (l, x), cs), p, l)

;; facts about adjusting clauses by adding literals and still getting valid resolvents

Theorem: resolvent-with-extra-literal-fact1b (validliteral (l) ∧ (l ∉ p2 ) ∧ (l ∈ r) ∧ validclause (p1 ) ∧ validclause (p2 ) ∧ validclause (p1list) ∧ resolvent-help (r, p1list, p1 , p2 )) → resolvent-help (r, p1list, p1 , cons (l, p2 ))

Theorem: resolvent-with-extra-literal-fact1c (validliteral (l) ∧ (l ∉ r) ∧ (l ∉ p2 ) ∧ validclause (p1 ) ∧ validclause (p2 ) ∧ validclause (p1list) ∧ resolvent-help (r, p1list, p1 , p2 )) → resolvent-help (cons (l, r), p1list, p1 , cons (l, p2 ))

Theorem: resolvent-with-extra-literal-fact2a ((l ∉ r) ∧ (l ∉ p1 ) ∧ validliteral (l) ∧ validclause (p1 ) ∧ validclause (p2 ) ∧ validclause (p1list) ∧ resolvent-help (r, p1list, p1 , p2 )) → resolvent-help (cons (l, r), p1list, cons (l, p1 ), p2 )

Theorem: resolvent-with-extra-literal-fact2b ((l ∈ r) ∧ (l ∉ p1 ) ∧ validliteral (l) ∧ validclause (p1 ) ∧ validclause (p2 ) ∧ validclause (p1list) ∧ resolvent-help (r, p1list, p1 , p2 )) → resolvent-help (r, p1list, cons (l, p1 ), p2 )

Theorem: resolvent-with-extra-literal-fact3a ((l ∉ r) ∧ (l ∉ p1 ) ∧ (l ∉ p2 ) ∧ validliteral (l)

∧ validclause (p1 ) ∧ validclause (p2 ) ∧ validclause (p1list) ∧ resolvent-help (r, p1list, p1 , p2 )) → resolvent-help (cons (l, r), p1list, cons (l, p1 ), cons (l, p2 ))

Theorem: resolvent-fact resolvent-help (a, b, c, d) → resolvent-help (cons (l, a), b, c, d)

Theorem: extra-try-resolvent-fact resolvent-help (a, b, c, d) → resolvent-help (a, cons (l, b), c, d)

Theorem: when-not-member-of-take-out-literal ((1 < length (c)) ∧ (a ∈ take-out-literal (x, c)) ∧ (a ∉ x)) → (cons (car (c), a) ∈ x)

Theorem: take-out-literal-is-validclause (validclauses (x) ∧ (1 < length (c))) → validclauses (take-out-literal (x, c))

Theorem: member-of-validclause-is-validlit (validclause (cs) ∧ (l ∈ cs)) → validliteral (l)

Theorem: when-literal-not-there (validclauses (cs) ∧ (x ∉ cs)) → (take-out-literal (cs, x) = cs)

Theorem: real-proof-implies-almost-proof validproof (cs, p) → validproof-but-for-literal (cs, p, x)

Theorem: when-not-in-bigger-clauses ((¬ set-member (x, cs)) ∧ set-member (x, take-out-literal (cs, p))) → set-equal (cdr (p), x)

Theorem: take-out-literal-produces-almost-proof (proof-form (p) ∧ validproof (take-out-literal (cs, c), p) ∧ validclauses (cs) ∧ (1 < length (c))) → validproof-but-for-literal (cs, p, car (c))

Theorem: member-of-validclauses-is-validclause (validclauses (x) ∧ (a ∈ x)) → validclause (a)

Theorem: find-contradiction-returns-proof-form ((¬ box-in-axioms (x)) ∧ (excess-literal (x) ≃ 0) ∧ unsatisfiable (x) ∧ validclauses (x)) → proof-form (list (find-contradiction (x)))

Theorem: proofs-together-have-form-if-both-do (proof-form (x) ∧ proof-form (y)) → proof-form (append (x, y))

Theorem: adjust-does-not-unform-proofs (proof-form (x) ∧ validliteral (l)) → proof-form (adjust (x, cs, l))

;; getproof returns something that is of a resolution proof form
;; (later we show that this proof is "valid")

Theorem: getproof-gives-proof-form (unsatisfiable (x) ∧ validclauses (x)) → proof-form (getproof (x))

Theorem: allunits-means-no-excess-literal allunits (x) → (excess-literal (x) ≃ 0)

Theorem: find-contradiction-returns-box (unsatisfiable (x) ∧ (¬ box-in-axioms (x)) ∧ (excess-literal (x) ≃ 0) ∧ validclauses (x)) → (car (find-contradiction (x)) = nil)

Theorem: last-element-fact listp (x) → (last-element (append (y, x)) = last-element (x))

Theorem: getproof-is-list-when (¬ box-in-axioms (x)) → listp (getproof (x))

;; the last resolvent in a getproof-generated proof is box

Theorem: getproof-returns-box (unsatisfiable (x) ∧ validclauses (x) ∧ (¬ box-in-axioms (x))) → (car (last-element (getproof (x))) = nil)

;; adjusting a proof ending in box yields a proof ending in box or a proof
;; whose last resolvent has just the literal used to adjust the proof

Theorem: adjusted-proof-gets (car (last-element (p)) = nil) → ((car (last-element (adjust (p, x, l))) = nil)

∨ (car (last-element (adjust (p, x, l))) = list (l)))

Theorem: what-adjusted-proof-returns (unsatisfiable (x) ∧ validclauses (x) ∧ (¬ box-in-axioms (x)) ∧ (car (last-element (adjust (getproof (x), y, l))) ≠ nil)) → (car (last-element (adjust (getproof (x), y, l))) = list (l))

;; adjusting an "almost" correct proof yields a correct proof

Theorem: adjusting-makes-proofs-valid (validliteral (l) ∧ proof-form (p) ∧ validclauses (cs) ∧ validproof-but-for-literal (cs, p, l)) → validproof (cs, adjust (p, cs, l))

Theorem: validproof-of-append (proof-form (x) ∧ proof-form (y) ∧ validclauses (cs) ∧ validproof (cs, x) ∧ validproof (append (listofcars (x), cs), y)) → validproof (cs, append (x, y))

Theorem: getproof-returns-validproof (unsatisfiable (x) ∧ validclauses (x)) → validproof (x, getproof (x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; the completeness theorem

Theorem: resolution-is-complete (unsatisfiable (x) ∧ validclauses (x)) → finishedproof (x, getproof (x))

Index

adding-literal-fact, 12 adding-literal-induct, 12 adjust, 7–9, 15, 16 adjust-does-not-unform-proofs, 15 adjust-is-listp-when, 8 adjusted-proof-gets, 15 adjusting-makes-proofs-valid, 16 allunit-means, 11 allunits, 11, 12, 15 allunits-if, 11 allunits-means-no-excess-litera

l, 15 assignment-interchangeable, 10

box-in-axioms, 4, 7–9, 11, 12, 14, 15

equals-has-same-members, 5 excess-literal, 7–9, 11, 12, 14, 15 excess-literal-in-terms-of-cdr, 8 extra-try-resolvent-fact, 14

find-contradiction, 7, 9, 12, 14, 15 find-contradiction-returns-box, 15 find-contradiction-returns-proo

f-form, 14 finishedproof, 4, 12, 16 first-non-unit, 6–9 first-non-unit-fact, 7 first-non-unit-fact2, 6

getproof, 9, 15, 16 getproof-gives-proof-form, 15 getproof-is-list-when, 15 getproof-returns-box, 15 getproof-returns-validproof, 16

is-last-element-means-member, 6

last-element, 4, 6, 9, 15 last-element-fact, 15 length, 4, 6–9, 11, 14 list-means-length-more-0, 4 listofcars, 5, 6, 16

member-is-setmember, 5 member-of-append-1, 6 member-of-validclause-is-validlit, 14 member-of-validclauses-is-valid

clause, 14 membership-of-append, 6 membership-on-subsets, 5

no-box-fact, 8

no-box-zero-el-fact, 9 no-excess-literal-proof, 12 not-box-when-clause-taken, 9 number-of-lits, 7, 8

proof-form, 9, 10, 14–16

proofs-together-have-form-if-bot h-do, 15

real-proof-implies-almost-proof, 14 resolution-is-complete, 16 resolvent, 3, 4, 12 resolvent-fact, 14 resolvent-help, 3, 13, 14 resolvent-with-extra-literal-fa

ct1b, 13 ct1c, 13 ct2a, 13 ct2b, 13 ct3a, 13

restriction-list-commutative, 11 reversible-nots-1, 11 reversible-nots-2, 11

set-equal, 2, 5–7, 10–12, 14

set-equal-self, 5 set-equals-fact, 5 set-member, 2, 4–6, 8, 12, 14 setmember-is-setmember-of-super

set, 5 stupid-lemma1, 6 stupid-lemma2, 6 stupid-lemma3, 6 subset, 1–3, 5–7, 10 subset-fact-1, 5 subset-is-transitive, 5 subset-of-append, 6 subset-of-self, 5 subset-of-takeouts-fact, 7 subset-of-union-fact-1, 5

take-out-clause, 6, 7, 9, 10 take-out-clause-fact, 9 take-out-clause-helper, 10 take-out-clause-preserves-valid

clauseness, 7 take-out-literal, 6–10, 14 take-out-literal-communative-so

rt-of, 7 take-out-literal-helper, 10 take-out-literal-is-validclause, 14 take-out-literal-preserves-vali

dclauseness, 7 take-out-literal-produces-almost

-proof, 14 takeout, 3, 5, 6, 11 takeout-fact1, 5 takeout-fact2, 6 takeout1, 5, 7

unit-clause-fact, 11 unsat-ignore-first-helper, 11 unsat-induct, 11 unsat-stepper, 10 unsatisfiable, 3, 10, 12, 14–16 unsatwith, 2, 3, 10–12

validclause, 2, 10–14 validclauses, 2, 7, 12, 14–16 validliteral, 2, 13–16 validproof, 3, 4, 10, 14, 16 validproof-but-for-literal, 12, 14, 16 validproof-but-for-literal-clau

ses-commutative, 12 validproof-clauses-commutative, 10 validproof-of-append, 16 validproof-on-subset, 10

what-adjusted-proof-returns, 15 when-first-non-unit-gives-clause, 8 when-literal-not-there, 14 when-not-in-bigger-clauses, 14 when-not-member-of-take-out-lite

ral, 14 when-take-out-clause-does-somet

hing, 9 when-take-out-literal-does-somet

hing, 8 when-unsatisfiable, 10 without-literal-still-unsatisfi

able, 10