Extended Resolution Signature (#2788)

* Extended Resolution Signature

While extended resolution is a fairly general technique, the paper
"Extended Resolution Simulates DRAT" / the drat2er uses exactly one new
type of rule: definitions of the form

    new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)

This PR adds axioms supporting this kind of definition, and adds a test
making use of those new axioms. The axioms support the following ideas:

   1. Introducing a **fresh** variable, defined in the form above
   2. Clausifying that definition to produce proofs of $$ n + 2 $$ new
      clauses in the form of two clauses, and a cnf with $$ n $$ clauses
   3. An axiom for unrolling the proof of the cnf into proofs of the
      original clauses.

* Addressing Yoni's comments

1. Added a new (trivial) test
2. Improved a bunch of documentation

* Update proofs/signatures/er.plf

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* Removed references to RATs from the signature

There are still a few references in the header comment.

* Aside on continuations

* Scrap the elision annotations

0 files changed, 0 insertions, 0 deletions