OKullmann/oklibrary — pull request #373 by MGwynne (2012-02-20 21:57:09+00:00)
Title: Ephp proof

Branch: ephp_proof.

Adding the resolution refutation of Cook's extended pigeon-hole formulas, along with the functions necessary to do this. Further plans have been moved in the branch "ephp_proof_plans", to try and make this pull request as short as possible. Also added standardised clause-sets for EPHP and output functions for these clause-sets.

The following remaining issues have been fixed:

1) The lack of explicit standardisation is fixed in e114fa877a9fbe34960c5537192d1e12a477db80.
2) The bug in the tests is fixed in 038b0b137d76e36bae7ba3a2c28188def37a7f47.
3) The structure of the Pigeonhole.mac file is improved in d9d1b8d59b3562711a79119d9ba2f1042bef8afd.
4) That the extension is truly a (blocked) extension is checked in c9cba88f4060aa18349923fc36dda4c9f8aa434d via 02e895f0a93de082a932f7d16f1b057124c86cac.

Matthew