部分構造論理は、計算機科学や複雑系科学など、科学の先端分野で、方法論的枠組を提供するものとして、近年著しい発展を遂げている論理である。
　だが、従来の部分構造論理の研究は、証明論的方法ではシークエント計算での研究に終始している。さらには、乗法的選言を含んだ古典的部分構造論理では、シークエント計算においてすらも非可換なシステムは考察されていない。また、考察されているほとんどのシステムはカット除去定理が成立するものであり、カット除去定理や標準化定理の成立しないことの意義や理由についての研究もほとんど行われていない。
　一方、シークエント計算と並ぶ重要な形式体系の一つである Getntzen 式は、仮定の除去を伴う推論規則の適用に際し除去される仮定の位置などの情報が必要となっており、証明図全体の状況を見極めるというグローバルな視点からの考察を容易にしている。
　このため、自然演繹を用いて、量子論理をはじめとする部分構造論理において、構造に関する推論規則が証明や推論のなかでどのような働きをしているかを考察している。