Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus.

Robert L. Constable, Wojciech Moczydlowski

Browse the full LFCS paper archive.