1997 Fiscal Year Annual Research Report
| Project/Area Number |
09740162
|
|---|
| Research Institution | Tokyo Woman's Christian University |
|---|
Principal Investigator |
永山 操 東京女子大学, 文理学部, 講師 (30237557)
|
|---|
| Keywords | Linear Logic / proof nets / strongly planarity / Correctness theorem / Lambek Calculus |
|---|
| Research Abstract |
昨年度までの、非可換なLinear Logicの証明図にあたるnon-commutative proof netsについての研究をさらに進めた。まず、今まであまり研究されていなかったnon-commutativeなsystemにおけるnetsの概念として、strongly planar marked nets導入し、そのwell-formed structureに対する必要充分条件について考察した。ここで、tree-likeな平面的グラフと、そのグラフによって仕切られるregionsとの条件を考えることにより、平面的グラフに対するオイラーの公式が適用できる。これにより、regionsがあるcondition(region condition)を満たす時、well-formed structureかどうかを調べるのに、旧来のswitching conditionにおいて行われたいた。サブグラフのacyclicityとconnectnessの検証がどちらか一方でよいことがわかった。さらにこのregion conditionのもとでは、switching conditionで考慮されるサブグラフの数も劇的に減らすことができた。旧来のswitching conditionでは、mをpar-linkの個数とすると、2のm乗個のサブグラフの検証が必要となる。しかし新しい必要充分条件では、L-only subgraphとR-only subgraphと呼ばれる2つのサブグラフの検証で充分である。これにより、定理として、marked netがwell-formedとなる必要十分条件は、Gがstrongly planarであり、region conditionを満たし、かつL-only subgraphとR-only subgraphがacyclicかconnectedのどちらか一方であることがわかった。さらに、これからCyclic Linear Logicのmultiplicative fragmentにおけるnon-commutative proof netの新しい特徴づけ定理も得られる。
このように、本年度は研究において大きな前進がみられた。来年度はさらにこれを進め、Non-commutative Linear LogicやLambek Calculusにおける定理の自動証明に適用できるような、具体的なアルゴリズムの研究を行っていきたい。
|
Research Products
(3 results)
-
[Publications] Misao NAGAYAMA Mitsuhiro OKADA: "Characterization Theorems for Multiplicative Fragment of Intuitionistic Non-Commutative Linear Logic(Preliminary Report)" 数解研講究録. 818. 60-69 (1997)
-
[Publications] Misao NAGAYAMA Mitsuhiro OKADA: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic" Theoretical Computer Science. (Special issue)(to appear). (1998)
-
[Publications] Misao NAGAYAMA: "A Normalization Theorem for BB'I" Notre Dame Journal of Formal Logic. (to appear). (1998)
