登入
選單
返回
Google圖書搜尋
Mechanizing Proof Theory
Gianluigi Bellin
Stanford University. Computer Science Department
其他書名
Resource-aware Logics and Proof Transformations to Extract Implicit Information
出版
Stanford University
, 1990
URL
http://books.google.com.hk/books?id=LbQgAQAAIAAJ&hl=&source=gbs_api
註釋
In Linear Logic, where classical logic is regarded as the limit of a resource-aware logic, long-standing issues in proof-theory have been successfully attacked. We are particularly interested in the system of proof-nets as a multiple-conclusion Natural Deduction system for Linear Logic. In Part I of this thesis we present a new set of tools that provide a systematic and uniform approach to different resource-aware logics. In particular, we obtain uniqueness of the normal form for Multiplicative and Additive Linear Logic (sections 3 and 4) and an extension of Direct Logic of interest for nonmonotonic reasoning (section 8).