The theory of meaning via dependent type semantics and its automatic verification

• Project/Area Number: 23K28142
• Project/Area Number (Other): 23H03452 (2023)
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Multi-year Fund (2024); Single-year Grants (2023)
• Section: 一般
• Review Section: Basic Section 61030:Intelligent informatics-related; Basic Section 60030:Statistical science-related; Sections That Are Subject to Joint Review: Basic Section60030:Statistical science-related , Basic Section61030:Intelligent informatics-related
• Research Institution: Ochanomizu University
• Principal Investigator: 戸次 大介 お茶の水女子大学, 基幹研究院, 教授 (90431783)
• Project Period (FY): 2023-04-01 – 2028-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥18,590,000 (Direct Cost: ¥14,300,000、Indirect Cost: ¥4,290,000); Fiscal Year 2027: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000); Fiscal Year 2026: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000); Fiscal Year 2025: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000); Fiscal Year 2024: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000); Fiscal Year 2023: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
• Keywords: 計算言語学 / 形式意味論 / 依存型意味論

Outline of Research at the Start

形式意味論の研究において、意味理論が多様な言語事実を俯瞰的に予測・説明することに成功しているか否かを評価する方法は存在するのか、という問いが存在する。本研究計画ではその問いに対し、依存型意味論(DTS)による証明論的意味論の枠組みと、日本語CCGパーザ、定理自動証明器、および日本語推論テストセットJSeM、の組み合わせによって、DTSの理論を実装によって自動的に検証する方法論を提案する。