On intuitionistic proof nets with additional rewrite rules and their approximations |
| |
Authors: | Satoshi Matsuoka |
| |
Affiliation: | aDepartment of Electrical and Computer Engineering, Faculty of Engineering, Nagoya Institute of Technology, Gokiso, Showa-Ku, 466-8555, Japan |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|