| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2012: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2011: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2010: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2009: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Research Abstract |
(1) A research program called algebraic proof theory for substructural logics is developed. It is shown that axioms of substructural logics form a hierarchy, and for logics at a lower level, the cut elimination theorem precisely corresponds to the closure under completions in the algebraic sense.
(2) The theory of ludics, a variant of game semantics that originates in linear logic, is reformulated from a computational and coalgebraic point of view. An interactive completeness theorem is proved for a proof system that corresponds to constructive classical propositional logic, and is applied to an interpretation of general recursive types in the sense of the type theory for programming languages
|
