Bruce Spencer, J. D. Horton
A binary resolution proof, represented as a binary tree, is irregular if some atom is resolved away and reappears on the same branch. We develop an algorithm, linear in the size of the tree, which detects whether reordering the resolutions in a given proof will generate an irregular proof. If so, the given proof is not minimal. A deduction system that keeps only minimal proofs retains completeness. We report on an initial implementation.