Implementation and evaluation of contextual natural deduction for minimal logic

Abstract

The contextual natural deduction calculus (NDc) extends the usual natural deduction calculus (ND) by allowing the implication introduction and elimination rules to operate on formulas that occur inside contexts. It has been shown that, asymptotically in the best case, NDc-proofs can be quadratically smaller than the smallest ND-proofs of the same theorems. In this paper we describe the first implementation of a theorem prover for minimal logic based on NDc. Furthermore, we empirically compare it to an equally simple ND theorem prover on thousands of randomly generated conjectures.