Discovery Sagaサイレントキーワード俯瞰

これまでの形式論理言語の証明概念では捉えられない「証明」の「形式」について検討を進めた。日常言語推論、図形-画像推論、概念推論、情報環境の説明可能性論証、意思決定に関わる論証などを手掛かりとした。日常言語による推論・論証の固有な諸問題の調査を進めた。また、日常言語の機械学習(特に深層学習）モデルによる推論とを比較した。これら二つと形式論理言語による推論との相違について調査を開始した。(以上、峯島-岡田）図形や画像などの非言語的視覚的表現が論理的オペレータを表現可能か、調査した。否定を表現することが可能かを峯島らが検討し、成果にまとめた。論理的否定を含む論理定項については、線形論理レベルでの証明論及び証明論的意味論の再精査を岡田が進め、次年度計画の証明論的準備が完成した。形式論理学をベースの「証明」では捉えられない、概念からの推論に着目した研究も進めた。概念からの推論とは、考察の対象となる概念そのものの特性に訴えて成り立つ推論のことである。形式論理学においては、こうした推論は当の概念の内容を規定するある種の「公理」を前提とする演繹として説明されるが、推論を実際に行う場合は、そうした形式論理に訴えることなく、あくまでも概念そのものの性質としてわれわれがある種の推論を「妥当」なものとして認めることがある。一つの方法として、R. Brandomによる「推論主義」の立場に対する批判的検討を行った。特に伊藤が論文の形でまとめた。情報科学の新しい検証問題において、広い意味で概念推論の立場が有効であると考えられる例があり岡田が(アルゴリズムのethical properties検証などの例で）調査を進めた。各種のアルゴリズムの説明可能性検証と証明との関係についても調査した。図的論理表現により意思決定・判断の支援を行う可能性についても図的証明という観点から岡田が検討を始めた。

【研究分担者】
伊藤遼	早稲田大学	文学学術院	准教授	(Kakenデータベース)
峯島宏次	慶應義塾大学	文学部(三田)	准教授	(Kakenデータベース)