Organization
School of Computing Associate Professor
Title
Associate Professor
External link
KASHIMA Ryo
Degree
-
Doctor of Science ( Tokyo Institute of Technology )
Research Interests
-
Mathematical Logic
Research Areas
-
Natural Science / Basic mathematics
Education
-
Tokyo Institute of Technology Science of Engineering
- 1991
Country： Japan
-
Tokyo Institute of Technology Graduate School, Division of Science and Engineering
- 1991
-
Tokyo Institute of Technology School of Science
- 1988
Country： Japan
Professional Memberships
-
日本数学会
-
Association for Symbolic Logic
-
Association for Symbolic Logic
Committee Memberships
-
日本数学会 数学基礎論分科会運営委員
2008
Papers
-
On the completeness and the decidability of strictly monadic second‐order logic
Kento Takagi, Ryo Kashima
Mathematical Logic Quarterly 66 ( 4 ) 438 - 447 2021.1
-
Term-Space Semantics of Typed Lambda Calculus
Ryo Kashima, Naosuke Matsuda, Takao Yuyama
Notre Dame Journal of Formal Logic 61 ( 4 ) 2020.11
-
Reduction Rules for Intuitionistic $${ { \lambda}{\rho } }$$ λ ρ -calculus
Ken-etsu Fujita, Ryo Kashima, Yuichi Komori, Naosuke Matsuda
Studia Logica 103 ( 6 ) 1225 - 1244 2015.12
-
An axiomatization of ECTL
R. Kashima
Journal of Logic and Computation 24 ( 1 ) 117 - 133 2013.3
Books
-
数理論理学
朝倉書店 2009 （ ISBN:9784254117653 ）
-
C言語による計算の理論
サイエンス社 2008 （ ISBN:9784781912141 ）
-
ゲーデルと20世紀の論理学・第３巻・不完全性定理と算術の体系
東京大学出版会 2007
-
数学基礎論講義-不完全性定理とその発展
日本評論社 1997
MISC
-
A proof of the completeness theorem for the modal logic with transitive closure of accessibility relation
RYO KASHIMA
Research Reports on Mathematical and Computing Sciences C-266 2009
-
A proof of the completeness theorem for the modal logic with transitive closure of accessibility relation
RYO KASHIMA
Research Reports on Mathematical and Computing Sciences C-266 2009
-
General models and completeness of first-order modal mu-calculus
Ryo Kashima, Keishi Okamoto
JOURNAL OF LOGIC AND COMPUTATION 18 ( 4 ) 497 - 507 2008.8
-
Sequent calculi for some strict implication logics
Ryo Ishigaki, Ryo Kashia
LOGIC JOURNAL OF THE IGPL 16 ( 2 ) 155 - 174 2008.4
-
Completeness Theorem of First-Order Modal mu-calculus
Ryo Kashima, Keishi Okamoto
Research Reports on Mathematical and Computing Sciences, TIT C-244 2007
-
中間述語論理CDについて
鹿島亮
京都大学数理解析研究所講究録 1533 2007
-
Completeness Theorem of First-Order Modal mu-calculus
Ryo Kashima, Keishi Okamoto
Research Reports on Mathematical and Computing Sciences, TIT C-244 2007
-
A Proof-Theoretical Study on Logics with Constructible Falsity (Sequent Calculi and Proof Theory)
Hasuo Ichiro, Kashima Ryo
RIMS Kokyuroku 1301 92 - 121 2003.1
-
A Proof-Theoretical Study on Logics with Constructible Falsity
Ichiro Hasuo, Ryo Kashima
Research Reports on Mathematical and Computing Sciences, TIT C-165 2003
-
On semilattice relevant logics
Ryo Kashima
Mathematical Logic Quarterly 49 ( 4 ) 401 - 414 2003
-
Sequent Calculi for Visser's Propositional Logics
Katsumasa Ishii Ryo, Kashima Kentaro Kikuchi
Notre Dame Journal of Formal Logic 42 ( 1 ) 1 - 22 2003
-
Kripke completeness of first-order constructive logics with strong negation
Ichiro Hasuo, Ryo Kashima
LOGIC JOURNAL OF THE IGPL 11 ( 6 ) 615 - 646 2003
-
A Proof-Theoretical Study on Logics with Constructible Falsity
Ichiro Hasuo, Ryo Kashima
Research Reports on Mathematical and Computing Sciences, TIT C-165 2003
-
On semilattice relevant logics
R Kashima
MATHEMATICAL LOGIC QUARTERLY 49 ( 4 ) 401 - 414 2003
-
Kripke Completeness of First-Order Constructive Logics with Strong Negation
Ichiro Hasuo, Ryo Kashima
Logic Journal of the Interest Group in Pure and Applied Logics 11 ( 6 ) 615 - 646 2003
-
Sequent Calculi for Visser's Propositional Logics
Katsumasa Ishii, Ryo Kashima, Kentaro Kikuchi
Notre Dame Journal of Formal Logic 42 ( 1 ) 1 - 22 2001.1
-
Proof Theoretical Studies on Semilattice Relevant Logics
Ryo Kashima
Research Reports on Mathematical and Computing Sciences, TIT C-157 2001
-
Proof Theoretical Studies on Semilattice Relevant Logics
Ryo Kashima
Research Reports on Mathematical and Computing Sciences, TIT C-157 2001
-
Completeness of implicational relevant logics
R Kashima
Logic Journal of IGPL 8 ( 6 ) 761 - 785 2000.11
-
A Proof of the Standardization Theorem in Lambda-Calculus
Ryo Kashima
Research Reports on Mathematical and Computing Sciences, TIT C-145 2000
-
Completeness of Implicational Relevant Logics
Ryo Kashima
Logic Journal of the IGPL 8 ( 6 ) 761 - 785 2000
-
A Proof of the Standardization Theorem in Lambda-Calculus
Ryo Kashima
Research Reports on Mathematical and Computing Sciences, TIT C-145 2000
-
Labelled sequent calculi and completeness theorems for implicational relevant logics
Ryo Kashima
Research Reports on Mathematical and Computing Sciences, TIT C-140 1999
-
Substructural Implicational Logics Including the Relevant Logic E
Ryo Kashima, Norihiro Kamide
Studia Logica 63 ( 2 ) 181 - 212 1999
-
Labelled sequent calculi and completeness theorems for implicational relevant logics
Ryo Kashima
Research Reports on Mathematical and Computing Sciences, TIT C-140 1999
-
Substructural Implicational Logics Including the Relevant Logic E
Ryo Kashima, Norihiro Kamide
Studia Logica 63 ( 2 ) 181 - 212 1999
-
Contraction-elimination for implicational logics
R Kashima
ANNALS OF PURE AND APPLIED LOGIC 84 ( 1 ) 17 - 39 1997.3
-
Contraction-Elimination for Implicational Logics
RYO KASHIMA
Annals of Pure and Applied Logic 84 17 - 39 1997
-
On the difficulty of writing out formal proofs in arithmetic
R Kashima, T Yamaguchi
MATHEMATICAL LOGIC QUARTERLY 43 ( 3 ) 328 - 332 1997
-
Cut-free sequent calculi for some tense logics
Ryo Kashima
Studia Logica 53 ( 1 ) 119 - 135 1994.3
-
Cut-Free Sequent Calculi for Some Tense Logics
RYO KASHIMA
Studia Logica 53 119 1994
-
CUT-ELIMINATION THEOREM FOR THE LOGIC OF CONSTANT DOMAINS
R KASHIMA, T SHIMURA
MATHEMATICAL LOGIC QUARTERLY 40 ( 2 ) 153 - 172 1994
-
Cut‐Elimination Theorem for the Logic of Constant Domains
Ryo Kashima, Tatsuya Shimura
Mathematical Logic Quarterly 40 ( 2 ) 153 - 172 1994
-
The Word Problem for Free BCI-Algebras Is Decidable
Ryo Kashima
Mathematica Japonica 37 1025 1992
-
The Word Problem for Free BCI-Algebra Is Decidable
Ryo Kashina, Yuichi Komori
Mathematica Japonica 37 1025 1992
Presentations
-
非古典論理のシーケント計算 ― 完全性定理のシーケント計算による証明
日本数学会 数学基礎論分科会 1999年度年会 1999
-
Semilattice Relevant Logics について
日本数学会2001年度秋季総合分科会数学基礎論分科会 2001
-
On the Standardization Theorem for Lambda-Beta-Eta-Calculus
International Workshop on Rewriting in Proof and Computation (RPC'01) 2001
-
On the Standardization Theorem for Lambda-Beta-Eta-Calculus
International Workshop on Rewriting in Proof and Computation (RPC'01) 2001
-
非反射的様相を持つ論理の完全性について
日本数学会2004年度秋季総合分科会 2004
-
Bimodal Logics with Irreflexive Modality
1st World Congress on Universal Logic 2005
-
Bimodal Logics with Irreflexive Modality
1st World Congress on Universal Logic 2005
-
中間命題論理の公理に関する問題
日本数学会年会 2006
-
述語様相μ計算の完全性について
日本数学会2007年度年会 2007
-
到達可能関係の推移的閉包を扱う様相論理の完全性
日本数学会 数学基礎論分科会 講演アブストラクト 2009
Works
-
様相μ計算に関する研究
2007
Research Projects
-
モデル検査のための構成的ミュー計算
Grant number：24KF0214 2024.11 - 2027.3
日本学術振興会 科学研究費助成事業 特別研究員奨励費
鹿島 亮
Grant amount：\2000000 （ Direct Cost: \2000000 ）
-
様相ミュー計算と確率ゲームへの逆数学的アプローチ：ハイブリッド検査法の創出と分析
Grant number：23K21641 2021.4 - 2023.3
日本学術振興会 科学研究費助成事業 基盤研究(B)
田中 一之, 宮部 賢志, 鹿島 亮, 木原 貴行
Grant amount：\17290000 （ Direct Cost: \13300000 、 Indirect Cost：\3990000 ）
本研究の目的は，モデル検査など論理学の応用技術において仮定される論理や集合の公理が何かを探査し，異なる技法の間の類似性や相異性を顕在化することで，ハイブリッド技術の創出を目指すものである．初年度(令和３年度)においては５つの領域に焦点を絞り，それぞれの課題を探求し，得られた知見を統合して多角的な検討を加えて，より高度な視点を得る計画であった．しかし，コロナ禍の行動制限により研究交流がほとんど行えず，とくに本研究で重要な役割を担う中国とシンガポールの協力者たちとの交流には長い空白ができてしまったので，代表者は北京の応用数学研究所に滞在して彼らとの交流基盤の回復に努め，体制が整うまで本研究を中断することにした．従って，本年度の研究も未完結であるが，個別課題ごとには次のような顕著な成果が得られた．
1. 様相μ計算の論理式は，演算子μ,νの入れ替わりが何回生じるかで分類される．μν型の論理式でもνμ型の論理式でも表現されるクラスΔ2はμ型とν型の論理式の超限的な組合せによって表せることを示す論文を出版した．さらに，様相μ計算の階層の崩壊を認識論理学の視点で分析し，無知の形式化を行った．2. 様相μ計算の階層が様相の種類によってどう変わるかを，真理値評価ゲームを用いて調べた．3. 確率的モデル検査は，検査法や評価アルゴリムがランダム化されたもので，ここではBlackwellゲームの一種として扱う．代表者が開発したWKLoの超準的手法を用いて，確率アルゴリズムを逆数学的に分析する研究を進めた．4. 決定木において，クエリの最小コストを最大化する入力分布（固有分布）について，より一般な木構造に対して固有分布を調べて論文にまとめた．さらにはグラフ構造への一般化を検討している．５. 確率アルゴリズムの視点から確率的推論を捕捉する独自の研究を目指しながら，先行研究の成果を整理した． -
nonclassical logics
Grant type：Competitive
-
ラムダ計算
Grant type：Competitive
-
非古典論理
Grant type：Competitive
-
lambda calculus
Grant type：Competitive