Graph rewriting for natural deduction and the proper treatment of variables

Abstract

This paper presents a graph implementation of natural deduction for rst-order intuitionistic logic. Studies on proof complexity and rewriting tend to focus solely on the structure of proofs and ignore the formulas that are the conclusions of each proof step. The current approach has the additional motivation of investigating the behaviour of variables, and to this end the formulas within a proof are preserved in the graph structure. The graph system treats assumptions and variables uniformly and has no need for the explicit constraints on variable occurrences that earned natural deduction the reputation of not being elegant.