• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

シークエント計算の新技法

Research Project

Project/Area Number 14740064
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field General mathematics (including Probability theory/Statistical mathematics)
Research InstitutionTokyo Institute of Technology

Principal Investigator

鹿島 亮  東京工業大学, 大学院・情報理工学研究科, 助教授 (10240756)

Project Period (FY) 2002 – 2004
Project Status Completed (Fiscal Year 2004)
Budget Amount *help
¥1,500,000 (Direct Cost: ¥1,500,000)
Fiscal Year 2004: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2003: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2002: ¥500,000 (Direct Cost: ¥500,000)
Keywordsシークエント計算 / 様相論理 / 厳密含意 / 完全性 / 数理論理学 / 直観主義論理 / 構成的否定
Research Abstract

主に以下の二つの結果を得た.
(1)通常の様相論理では,様相記号はクリプキモデル上で二項関係(Rとする)によって真理値が定義されるが,これに「Rかつ≠」という関係で解釈される様相記号を追加する議論が最近,佐野勝彦氏(京大)を中心にして盛んになされている.
当科研費による研究では,そのようないくつかの様相論理の完全性を木状の構造を持ったシークエント計算を用いて証明した.
佐野氏はすでにカノニカルモデルによる従来の手法によって完全性を示していたが,対象となる論理に応じて従来の手法の方が簡潔にできる場合と木状シークエント計算の手法の方が簡潔にできる場合とがはっきりと分かれるという現象が明らかになった.
たとえば「推移的モデル」に対応する論理は前者,「推移的かつ反対称的モデル」に対応する論理は後者である.この違いが論理のどんな性質を反映しているのか興味深い問題であり,今後の解明が待たれる.
(2)直観主義論理のクリプキモデルの「反射的,推移的,遺伝的」という条件を変化させると,対応する論理も変わってくる.
これらは「厳密含意を持つ論理」と総称されている.
本研究ではそのような多くの論理に対して新たなシークエント計算体系を統一的に与え,完全性定理を証明した.さらに「遺伝的」の双対概念である「偽の遺伝性」に着目して,そのようなモデルを持つ論理と古典論理との関係を明らかにした.
またそれらの論理式ベースの体系化(ヒルベルト流体系)が,実質含意記号を使えば簡単であるが使わなければ困難であることを示した.

Report

(3 results)
  • 2004 Annual Research Report
  • 2003 Annual Research Report
  • 2002 Annual Research Report
  • Research Products

    (7 results)

All 2004 Other

All Journal Article (2 results) Publications (5 results)

  • [Journal Article] 非反射的様相を持つ論理の完全性について2004

    • Author(s)
      鹿島 亮
    • Journal Title

      日本数学会2004年度秋季総合分科会,数学基礎論および歴史分科会講演アブストラクト集

      Pages: 24-25

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Completeness via labelled sequent calculi for bimodal logics with irreflexive modality.2004

    • Author(s)
      Ryo Kashima
    • Journal Title

      Proceedings of 38th MLG meeting at Gamagori

      Pages: 53-55

    • Related Report
      2004 Annual Research Report
  • [Publications] Ryo Kashima: "On Semilattice Relevant Logics"Mathematical Logic Quarterly. 49・4. 401-414 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Katsumasa Ishii, Ryo Kashima, Kentaro Kikuchi: "Sequent Calculi for Visser's Propositional Logics"Notre Dame Journal of Formal Logic. 42・1. 1-22 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Ryo Kashima: "A cut-free sequent calculus with ε-symbols"Proceedings of the 36th MLG meeting at Kinosaki, Japan, 2002. 6-7 (2003)

    • Related Report
      2002 Annual Research Report
  • [Publications] Ichiro Hasuo, Ryo Kashima: "A proof-theoretical study on logics with constructible falsity"京都大学数理解析研究所講究録. 1301. 92-121 (2003)

    • Related Report
      2002 Annual Research Report
  • [Publications] Ryo Kashima: "On semilattice relevant logics"Mathematical Logic Quarterly. 49・4(予定). (2003)

    • Related Report
      2002 Annual Research Report

URL: 

Published: 2002-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi