Finding shortest proofs: An application of linked inference rules
In this article, we describe a procedure for systematically searching for shortest proofs in logical systems based on the inference rule condensed detachment. The procedure relies on applications of linked UR-resolution and uses demodulation to categorize derivations. Although the procedure is exhaustive in nature - and therefore realistically is applicable only to relatively small problems - it is shown to overcome the obstacles to finding shortest proofs presented by ordinary resolution-style theorem proving.
shortest proofs condensed detachment linked ur-resolution