项目名称: 基于格值逻辑的α-锁归结与α-锁调解自动推理

项目编号: No.61305074

项目类型: 青年科学基金项目

立项/批准年度: 2014

项目学科: 自动化技术、计算机技术

项目作者: 何星星

作者单位: 西南交通大学

项目金额: 22万元

中文摘要: 本项目围绕带等词的格值逻辑系统,研究启发式动态配锁策略下的α-锁归结与α-锁调解自动推理理论、方法和算法,设计相应的自动推理程序。主要内容包括:一、研究格值命题逻辑系统中广义文字的结构、典型类广义文字的归结域及其归结文字个数的选择。二、针对α-锁归结与α-广义锁归结方法,提出启发式动态配锁策略。在该策略下,分别建立两种锁归结方法的可靠性与完备性。三、针对带等词的逻辑公式,建立基于格值一阶逻辑的α-锁调解自动推理理论和方法,并建立该调解方法在启发式动态配锁策略下的可靠性与完备性。四、针对上述理论和方法,设计基于格值逻辑的自动推理程序。项目预期的成果有望为基于格值逻辑的自动推理研究提供新的思路,为定理机器证明、形式化验证等应用方面提供理论基础和实用工具。

中文关键词: 格值逻辑;α-自动推理;α-锁归结;α-锁调解;启发式策略

英文摘要: The present project focuses on efficient α-lock resolution-based and α-lock paramodulation-based automated reasoning with heuristically dynamic indexing strategies, which includes their theories, approaches, algorithms and utility procedures for lattice-valued logic with equality. Fristly, the structure of generalized literals, the resolution field of some typical generalized literals, and the criterion for selecting number of resolved generalized literals are given. Secondly, heuristically dynamic indexing strategies for α-lock resolution and α-generalized lock resolution are proposed, the soundness and completeness of these resolution methods are established. Thridly, α-lock paramodulation automated reasoning for handling lattice-valued logical formulae with equality is proposed. The soundness and completeness of α-lock paramodulation method with heuristically dynamic indexing strategy are given. According to the above results, the automated reasoning algorithm and procedure for lattice-valued logic are contrived. This work may provide an effective support for automated reasoning scheme in lattice-valued logic based on lattice implication algebra with the aim at establishing theoritical foundation and practical tools for mechanical theorem proving, formal verification and some other fields.

英文关键词: Lattice valued logic;α-Automated reasoning;α-Lock resolution;α-Lock paramodulation;Heuristic Searching strategies

成为VIP会员查看完整内容
0

相关内容

专知会员服务
71+阅读 · 2021年10月15日
专知会员服务
92+阅读 · 2021年6月23日
干货书《金融数学导论: 概念与计算方法》,290页pdf
专知会员服务
59+阅读 · 2021年5月7日
专知会员服务
67+阅读 · 2021年4月27日
【经典书】数理统计学,142页pdf
专知会员服务
94+阅读 · 2021年3月25日
【康奈尔】最新《强化学习基础》CS 6789课程
专知会员服务
66+阅读 · 2020年9月27日
【经典书】统计学,806页pdf,解锁数据的力量
专知会员服务
78+阅读 · 2020年8月12日
【硬核书】不完全信息决策理论,467页pdf
专知会员服务
334+阅读 · 2020年6月24日
从供应链中台的故事说起,聊一聊中台的本质和设计之道
人人都是产品经理
0+阅读 · 2022年1月16日
【AAAI 2022】神经分段常时滞微分方程
专知
2+阅读 · 2022年1月14日
【开放电子书】概率编程导论,301页pdf
专知
4+阅读 · 2021年10月21日
【WWW2021】基于知识嵌入的图卷积网络
专知
0+阅读 · 2021年4月27日
已删除
将门创投
12+阅读 · 2019年7月1日
零基础概率论入门:最大似然估计
论智
12+阅读 · 2018年1月18日
知识图谱实战
炼数成金订阅号
65+阅读 · 2017年12月6日
关系推理:基于表示学习和语义要素
计算机研究与发展
18+阅读 · 2017年8月22日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
2+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
1+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2022年4月20日
Arxiv
15+阅读 · 2021年2月19日
Hierarchical Graph Capsule Network
Arxiv
20+阅读 · 2020年12月16日
Arxiv
23+阅读 · 2018年10月24日
Arxiv
26+阅读 · 2018年2月27日
小贴士
相关VIP内容
专知会员服务
71+阅读 · 2021年10月15日
专知会员服务
92+阅读 · 2021年6月23日
干货书《金融数学导论: 概念与计算方法》,290页pdf
专知会员服务
59+阅读 · 2021年5月7日
专知会员服务
67+阅读 · 2021年4月27日
【经典书】数理统计学,142页pdf
专知会员服务
94+阅读 · 2021年3月25日
【康奈尔】最新《强化学习基础》CS 6789课程
专知会员服务
66+阅读 · 2020年9月27日
【经典书】统计学,806页pdf,解锁数据的力量
专知会员服务
78+阅读 · 2020年8月12日
【硬核书】不完全信息决策理论,467页pdf
专知会员服务
334+阅读 · 2020年6月24日
相关资讯
从供应链中台的故事说起,聊一聊中台的本质和设计之道
人人都是产品经理
0+阅读 · 2022年1月16日
【AAAI 2022】神经分段常时滞微分方程
专知
2+阅读 · 2022年1月14日
【开放电子书】概率编程导论,301页pdf
专知
4+阅读 · 2021年10月21日
【WWW2021】基于知识嵌入的图卷积网络
专知
0+阅读 · 2021年4月27日
已删除
将门创投
12+阅读 · 2019年7月1日
零基础概率论入门:最大似然估计
论智
12+阅读 · 2018年1月18日
知识图谱实战
炼数成金订阅号
65+阅读 · 2017年12月6日
关系推理:基于表示学习和语义要素
计算机研究与发展
18+阅读 · 2017年8月22日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
2+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
1+阅读 · 2008年12月31日
微信扫码咨询专知VIP会员