OKullmann/oklibrary — pull request #361 by MGwynne (2012-02-17 12:27:02+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 issues mentioned in rejection e-mails for this branch are fixed in the following commits:

1) Statistics functions now use closed form expressions rather than summations, in 6289b24b8c8076ae28ceb4a2c50dc96fb9b72a51 and d5ada62ad93c4e9d2d8d33d7a64d636faf119cd8.

2) The name "rename_php_var2ephp_var_cs" has been changed to "var_php2ephp_sm" in 56a950bedc0cfe9906b3a6592d780acd274492d6.

3) The commit message "Converting EPHP proof to proof using uniform variables" has been changed to "Converting EPHP proof to proof using a uniform variable naming scheme" in af96497a29609d421423c13bf0214e8109576ddf to make clearer the meaning.

4)&5) Haven't been included in this commit to avoid a pull request that is longer and so more likely rejected. They are being worked on on branch "ephp_proof_plans".

Matthew