- 著者
-
石原 啓子
平石 邦彦
- 出版者
- 一般社団法人電子情報通信学会
- 雑誌
- 電子情報通信学会技術研究報告. COMP, コンピュテーション
- 巻号頁・発行日
- vol.96, no.585, pp.41-50, 1997-03-17
最近、線形論理とペトリネットとの間の関係を調べる研究がされており、種々の結果が得られている。線形論理はresource consciousな論理であるということより、むしろ並行性を表すのに非常に有効な論理であると考えられている。線形論理において、ペトリネットのplaceとtransitionはそれぞれ論理式と証明可能性に関係づけられる。EngbergとWinskelは、直観主義線形論理のモデルとして、直接ペトリネットからquantaleを生成することにより双方の関係を調べた。彼らは、このペトリネットより生成されたquantaleに対する、直観主義線形論理の健全性を示したが、完全性の証明は示していなかった。ここで我々は、ペトリネットよりquantaleを生成する新たな方法を示し、直観主義線形論理の完全性を証明した。