On intuitionistic proof nets with additional rewrite rules and their approximations
Satoshi Matsuoka · Electronic Notes in Theoretical Computer Science · 2001
First we present a proof nets system with eight additional rewrite rules, which concerns ordering of introductions of exponential-links and are only applied to normal forms of proof nets in the usual sense. We show that the reduction relation generated by these eight rewrite rules is strong normalizing and confluent. Second we propose an simply judged equality on intuitionistic proof nets based on the notion of the main path of an intuitionistic proof net. The notion is an analogue of Böhm-trees in λ-calculus.