STUDIES ON REASONING PRINCIPLE BASED ON LOGICAL FRAMEWORK THEORY AND ITS APPLICATION TO HEURISTIC REASONING SYSTEM
基于逻辑框架理论的推理原理研究及其在启发式推理系统中的应用
基本信息
- 批准号:07680405
- 负责人:
- 金额:$ 1.28万
- 依托单位:
- 依托单位国家:日本
- 项目类别:Grant-in-Aid for Scientific Research (C)
- 财政年份:1995
- 资助国家:日本
- 起止时间:1995 至 1996
- 项目状态:已结题
- 来源:
- 关键词:
项目摘要
In 1995, I have researched by focussing on the studies on the reasoning prrinciple based on the logical framework theory and intelligent language construction for intelligent reasoning systems. In 1996, I have researched mainly on the following themes from the viewpoints of inplemention of the heuristic reasoning system using the results obtained until now.(1) Studies on language for Artificial intelligence based on the logical framework theory : Using the logical framework theory, I have investigated problems such that knowledge and data representation method, and the theoretical properties of inheritance mechanism which is essential for efficient system construction. An experimental language has been implemented according to the obtained results on the SUN workstation.(2) Automatic proof generation based on the type theory : The relations between the type inference system and the LK sequent calculus has been investigated, and the problems of higher order proof method and unification theory are also discussed. Further, a method of producing a proof automaticaliy using the formulas as types principle in the type theory has been proposed and is formulated in the grammatical form.(3) Proof discovery system based on analogy : A system which reasons and discover a proof of the first order sequent calculus in the similar mannar to human beings is implemented using a general theorem proving language ISABELLE on the SUN work station.It has been recognized that the approach based on the logical framework theory is useful to formalize the reasoning principle and intelligent language through this research. I am planning to extend this approch for AI further.
1995年,我主要研究了基于逻辑框架理论的推理原理和智能推理系统的智能语言构造。1996年,我从实现启发式推理系统的角度出发,主要研究了以下几个主题:(1)基于逻辑框架理论的人工智能语言研究:利用逻辑框架理论,研究了知识和数据的表示方法,以及有效构建系统所必需的继承机制的理论性质等问题。(2)基于类型理论的证明自动生成:研究了类型推理系统与LK序列演算之间的关系,讨论了高阶证明方法和合一理论问题。(3)基于类比的证明发现系统:在SUN工作站上使用通用定理证明语言Isabelle实现了一个推理和发现类似于人类的一阶序列演算证明的系统。通过本研究,认识到基于逻辑框架理论的方法对于形式化推理原理和智能语言是有用的。我计划将这一方法进一步扩展到人工智能。
项目成果
期刊论文数量(4)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
原尾政輝: "順序付型理論による継承の定式化" 電気関係学会九州支部大会論文集. 1995年度. 1331-1331 (1995)
Masateru Harao:“使用有序类型理论进行继承”,日本电气工程学会九州分会会议记录,1995 年。1331-1331 (1995)。
- DOI:
- 发表时间:
- 期刊:
- 影响因子:0
- 作者:
- 通讯作者:
原尾政輝: "高階順序ソ-ト型理論における部分型と継承の意味論" 電子情報通信学会技術報告. COMP95-28. 19-28 (1995)
Masateru Harao:“高阶排序类型理论中的子类型和继承”IEICE 技术报告 19-28 (1995)。
- DOI:
- 发表时间:
- 期刊:
- 影响因子:0
- 作者:
- 通讯作者:
原尾政輝: "型理論に基づく知識表現言語の実現" 人工知能学会全国大会論文集. 9. 13-16 (1995)
Masateru Harao:“基于类型理论的知识表示语言的实现”日本人工智能学会全国会议论文集 9. 13-16 (1995)。
- DOI:
- 发表时间:
- 期刊:
- 影响因子:0
- 作者:
- 通讯作者:
山田,平田,原尾: "型付きラムダ計算における証明文法" 電子情報通信学会技術報告. COMP95-58. 11-20 (1995)
Yamada、Hirata、Harao:“类型化 lambda 演算中的证明语法”IEICE COMP95-58 (1995)。
- DOI:
- 发表时间:
- 期刊:
- 影响因子:0
- 作者:
- 通讯作者:
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
HARAO Masateru其他文献
HARAO Masateru的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('HARAO Masateru', 18)}}的其他基金
A General Study On Intelligent Reasoning Principles and Programming Languages For Artificial Intelligence.
人工智能智能推理原理与编程语言综述。
- 批准号:
07308027 - 财政年份:1995
- 资助金额:
$ 1.28万 - 项目类别:
Grant-in-Aid for Scientific Research (A)
Formalization of Higher Order Ingerence Mechanism Based on Type Theory and Its Application to Analogical Reasoning System
基于类型论的高阶推理机制形式化及其在类比推理系统中的应用
- 批准号:
04650320 - 财政年份:1992
- 资助金额:
$ 1.28万 - 项目类别:
Grant-in-Aid for General Scientific Research (C)
Higher Order Unification and Mechanization of Higher Order Theorem Proving System
高阶定理证明系统的高阶统一与机械化
- 批准号:
01580020 - 财政年份:1989
- 资助金额:
$ 1.28万 - 项目类别:
Grant-in-Aid for General Scientific Research (C)
Design of a System Description Language based on a Temporal-Spatiol Modal Logic and its Application to Automated Circuit Synthesis Problems.
基于时空模态逻辑的系统描述语言的设计及其在自动电路综合问题中的应用。
- 批准号:
60580016 - 财政年份:1985
- 资助金额:
$ 1.28万 - 项目类别:
Grant-in-Aid for General Scientific Research (C)
相似海外基金
Conference: Student Support for Second International Conference on Homotopy Type Theory (HoTT 2023)
会议:第二届同伦类型理论国际会议 (HoTT 2023) 的学生支持
- 批准号:
2318492 - 财政年份:2023
- 资助金额:
$ 1.28万 - 项目类别:
Standard Grant
[infinite]-Lie Groups and Their [infinite]-Lie Algebras in Real Cohesive Homotopy Type Theory
实内聚同伦型理论中的[无穷]-李群及其[无穷]-李代数
- 批准号:
2888102 - 财政年份:2023
- 资助金额:
$ 1.28万 - 项目类别:
Studentship
Homotopy theory, homotopy type theory and higher topos theory
同伦理论、同伦类型理论和更高层次的拓扑理论
- 批准号:
RGPIN-2022-04739 - 财政年份:2022
- 资助金额:
$ 1.28万 - 项目类别:
Discovery Grants Program - Individual
Homological algebra in homotopy type theory
同伦型理论中的同调代数
- 批准号:
574650-2022 - 财政年份:2022
- 资助金额:
$ 1.28万 - 项目类别:
University Undergraduate Student Research Awards
Investigating Inductive Types within Dependent Type Theory
研究依赖类型理论中的归纳类型
- 批准号:
2594512 - 财政年份:2021
- 资助金额:
$ 1.28万 - 项目类别:
Studentship
Homotopy Type Theory, Higher Category Theory
同伦类型论、高范畴论
- 批准号:
2431961 - 财政年份:2020
- 资助金额:
$ 1.28万 - 项目类别:
Studentship
Summer School on Homotopy Type Theory 2019
同伦类型论暑期学校 2019
- 批准号:
1912896 - 财政年份:2019
- 资助金额:
$ 1.28万 - 项目类别:
Standard Grant
Modal type theory and Higher-dimensional algebra
模态类型理论和高维代数
- 批准号:
2119874 - 财政年份:2018
- 资助金额:
$ 1.28万 - 项目类别:
Studentship