On the intuitionistic force of classical search

Abstract

The combinatorics of proof-search in classical propositional logic lies at the heart of most efficient proof procedures because the logic admits least-commitment search. The key to extending such methods to quantifiers and non-classical connectives is the problem of recovering this least-commitment principle in the context of the non-classical/non-propositional logic; i.e., characterizing when a least-commitment (classical) search yields sufficient evidence for provability in the (nonclassical) logic. In this paper, we present such a characterization for the (⊃, ∧)-fragment of intuitionistic logic using the λμ-calculus: a system of realizers for classical free deduction (cf. natural deduction) due to Parigot. We show how this characterization can be used to define a notion of uniform proof, and a corresponding proof procedure, which extends that of Miller et al. to multiple-conclusioned sequent systems. The procedure is sound and complete for the fragment of intuitionistic logic considered and enjoys the combinatorial advantages of search in classical logic.