Partial Proof Terms in the Study of Idealized Proof Search

We show that the Curry-Howard methodology of representation of finished proofs by means of proof terms can be slightly extended to become a tool in the theoretical study of proof search, where no considerations of control, effectiveness or implementation are made, but where the representation of partial (i.e. incomplete) proofs and their conversion into finished proofs is central. We propose partial proof terms, which are proof terms expressing gaps with the help of formal sequents, the latter being sequents occurring as proper components of the syntax of proof terms. We can specify proof search procedures as rewriting systems acting on partial proof terms; and we can extend a given logical system to one dealing with partial proof terms, becoming a calculus of partial derivations whose sequents express proof states, comprising a goal sequent, a record of the history of the search, and a list of proof obligations. The main goal of the paper is to illustrate the methodology at work. We consider two examples: the sequent calculus LJT, whose proof search procedure is focusing, and a bidirectional natural deduction system we call NJT, whose proof search procedure follows the ideas of the intercalation calculus. Focusing in LJT uses formal sequents just to represent holes in the proof, while intercalation, with its combination of bottom-up and top-down reasoning, needs in some stages the representation of more sophisticated, history sensitive, situations. We prove focusing isomorphic to intercalation using the tools we propose.