位置：立项数据库 > 立项详情页
基于tableau的非经典逻辑经典化的自动定理证明研究
  • 项目名称：基于tableau的非经典逻辑经典化的自动定理证明研究
  • 项目类别：面上项目
  • 批准号：60873116
  • 申请代码：F020107
  • 项目来源：国家自然科学基金
  • 研究期限：2009-01-01-2011-12-31
  • 项目负责人：刘全
  • 负责人职称：教授
  • 依托单位：苏州大学
  • 批准年度：2008
中文摘要：

自动定理证明是涉及人类智能问题的重要研究课题之一，对人工智能的研究具有重要的影响和推动作用。本项目针对非经典逻辑缺乏有效的自动定理证明过程的问题，提出将非经典逻辑通过转化，用经典逻辑进行tableau自动定理证明的方法。该方法在经典逻辑的基础上，将逻辑强化学习、归纳逻辑程序设计、布尔剪枝、等式合一、等价翻译等方法应用于非经典逻辑中，使得复杂的非经典逻辑定理可以在经典层面上来证明。一方面，一些提高经典逻辑证明效率的方法，可以应用到非经典逻辑中；另一方面，一些经典逻辑自动定理证明系统只要稍加改动就很容易扩展成为非经典逻辑系统。本项目的研究成果将在符号自动定理证明理论和方法上有所贡献，可以有效地扩大tableau推理的适用范围，在时间和空间上提高证明效率，更大程度地减少tableau扩展的盲目性和不确定性。

中文主题词： 非经典逻辑；经典化；tableau；自动定理证明
成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 39
  • 13
  • 0
  • 0
  • 0
期刊论文
A Bit-decomposition Adaptive Watermarking Algorithm Based on the Multi-Polar Mask
Global and local convergence of a class of penalty-free-type methods for nonlinear programming
关系强化学习方法的初步研究
一种局部的重叠社区发现方法
一种基于粗糙集的社区结构发现算法
基于布尔矩阵的Deep Web复杂模式匹配
遗传反馈的多特征图像检索
基于角点特征的几何同步数字水印算法
一种动态挥发率和启发式修正的蚁群优化算法
基于强化学习的多策略选择遗传算法
最小状态变元平均奖赏的强化学习方法
基于角点特征的集合同步数字水印算法
一种基于启发式奖赏函数的分层强化学习方法
Relevance feedback techniques and genetic algorithm for image retrieval based on multiple features.
Double elite co-evolutionsry genetic algorithm
利用tableau方法修正Deep Web中不相容知识
Convergence of Affine-scaling Interior-point Methods with Line Search for Box Constrained Optimizati
一种大规模离散空间中的高斯强化学习方法
双精英协同进化遗传算法
基于时间窗的自适应核密度估计运动检测方法
非清晰区域抑制下的显著对象检测方法
基于相变和似然性的多相图像分割方法
一种基于线性函数逼近的离策略Q（λ）算法
一种多分类器Deep Web数据源的自动分类与判别方法
融合目标特征和空间信息的粒子滤波跟踪
基于总体变分修复模型的图像编码
基于分段多高斯和辐射模板的人脸检测
一阶逻辑公式自动推演前的预处理
一种用于二维流体表面绘制算法的研究
基于Bayes序贯估计的无线传感器网络数据融合算法
一种基于图的颜色纹理区域分割方法
快速3D-MSPIHT视频编码算法
聚类差分图像核密度估计前景目标检测
传感器网络病毒感染传播局域控制研究
不规则扁平粒状物表面平整度识别与分选方法的研究
会议论文
An Improved Algorithm of Decision Trees for Streaming Data Based on VFDT
A Gaussian Processes Reinforcement Learning Method in Large Discrete State Spaces
A Reinforcement Learning Algorithm based on Minimum State Method and Average Reward
Correlated-clustering Frame: A Holistic Method of Deep Web Schema Matching Based on Data Mining
Decision Tree Merging Branched Algorithm Based on Equal Predictability
The Discovery and Extraction of Query Interfaces Based on Deep Web
Decision Tree Algorithm Based on Average Euclidean Distance
A method to automatic discover and classify Deep Web data source using Multi-classifier
A Hierarchical Reinforcement Learning Algorithm Based on Heuristic Reward Function
A Fast OBS Algorithm Based on Pseudo-Entropy of Weights
An Ant Colony Optimization Algorithm Based on Dynamic Evaporation Rare Fitting
The Research on the Spider of the Domain-Specific Search Engines Based on the Reinforcement Learning
Using Statistical Network Link Model for Routing in Ad Hoc Networks with multi-agent Reinforcement L
相关项目
非Tarski模型定理机器证明
期刊论文 16 会议论文 7
非经典逻辑的自动推理
期刊论文 13 会议论文 1
面向携带证明软件设计的语言、逻辑和证明
期刊论文 35 会议论文 10
刘全的项目
基于模糊逻辑的大规模强化学习理论及方法
期刊论文 10
　DeepWeb中不完备知识处理的理论及方法研究
面向tableau模型的逻辑强化学习理论及方法研究
期刊论文 41 专利 2
基于贝叶斯推理的模糊逻辑强化学习模型研究
期刊论文 31
基于部分感知模型的贝叶斯强化学习理论及方法
　DeepWeb中不完备知识处理的理论及方法研究
近红外波段堆垛结构三维光子晶体的制备和研究
期刊论文 2 会议论文 6 获奖 2 专利 5