含等词的超表演算

含等词的超表演算

冯莎莎^1,2, 孙吉贵^1,2, 吴瑕¹

1. 吉林大学计算机科学与技术学院, 长春 130012; 2. 吉林大学符号计算与知识工程教育部重点实验室, 长春 130012

收稿日期:2004-12-13 修回日期:1900-01-01 出版日期:2005-07-26
通讯作者: 孙吉贵

Hyper Tableau with Equality

FENG Sha-sha^1,2, SUN Ji-gui^1,2, WU Xia¹

1. College of Computer Science and Technology, Jilin University, Changchun 130012, China;2. Key Laboratory of Symbolic Computation and Knowledge Engineer of Ministry of Education, Jilin University, Changchun 130012, China

Received:2004-12-13 Revised:1900-01-01 Online:2005-07-26
Contact: SUN Ji-gui

摘要/Abstract

摘要： 将处理等词问题的Superposition方法引入超表演算中, 使超表演算能处理含等词的一阶逻辑问题, 这种新的表演算不但具有完备性, 而且无需回溯, 是用表演算完成含等词的一阶逻辑定理机器证明的一种尝试.

关键词: 超表演算, Superposition方法, 等词

Abstract: The hyper tableau calculus is capable of solving first -order logic problems with equality by introducing superposition to it, which i s competent in equality reasoning. The new tableau calculus is backtrack-free a s well as complete. It is an attempt at completing the machine proving of the fi rst-order logic theorem with equality via the tableau calculus.

Key words: hyper tableau calculus, superposition method, equality

中图分类号:

TP31

冯莎莎, 孙吉贵, 吴瑕. 含等词的超表演算[J]. J4, 2005, 43(04): 455-460.

FENG Sha-sha, SUN Ji-gui, WU Xia. Hyper Tableau with Equality[J]. J4, 2005, 43(04): 455-460.

[1]	杨光, 贾焱鑫, 陈翔, 许舒源. 基于深度学习的Stack Overflow问题帖分类方法[J]. 吉林大学学报(理学版), 2021, 59(4): 922-928.
[2]	李芳, 曲豫宾, 陈翔, 李龙, 杨帆. 一种基于类不平衡学习的情感分析方法[J]. 吉林大学学报(理学版), 2021, 59(4): 929-935.
[3]	曲豫宾, 陈翔, 李龙. 可缓解类重叠问题的跨版本软件缺陷预测方法[J]. 吉林大学学报(理学版), 2021, 59(2): 372-378.
[4]	何锴琦, 马宇骁, 张炎, 刘华虓. 一种基于数据的GitHub项目个性化混合推荐方法[J]. 吉林大学学报(理学版), 2020, 58(6): 1399-1406.
[5]	胡黄水, 赵思远, 刘清雪, 王出航, 王婷婷. 基于动量因子优化学习率的BP神经网络PID参数整定算法[J]. 吉林大学学报(理学版), 2020, 58(6): 1415-1420.
[6]	穆翔宇, 范钰, 李苏吉, 张鹏, 刘磊. 一种基于梯度下降算法的蜕变关系生成方法[J]. 吉林大学学报(理学版), 2020, 58(6): 1429-1435.
[7]	王壹铭, 初剑峰, 王永军, 陈彦东. 基于有向无环图的高效区块链共识算法[J]. 吉林大学学报(理学版), 2020, 58(5): 1167-1172.
[8]	汤战勇, 郝杰, 郭军, 刘宝英. 基于变步长随机行走算法的IC电源网络动态分析[J]. 吉林大学学报(理学版), 2020, 58(4): 868-876.
[9]	骆焦煌. 基于卷积神经网络的粗粒度数据分布式算法[J]. 吉林大学学报(理学版), 2020, 58(4): 906-912.
[10]	吴春琼. 面向大规模数据的特征趋势推理算法[J]. 吉林大学学报(理学版), 2020, 58(2): 364-370.
[11]	史肖冰, 郭德贵, 曹捷. 基于自适应Hata模型的无线电发射源定位方法[J]. 吉林大学学报(理学版), 2020, 58(1): 109-112.
[12]	楚玺, 周志祥, 邓国军, 邵帅. 模糊图像的不连续边缘智能检测改进算法[J]. 吉林大学学报(理学版), 2019, 57(04): 875-881.
[13]	刘良凤, 刘三阳. 基于权重差异度的动态模糊聚类算法[J]. 吉林大学学报(理学版), 2019, 57(3): 574-582.
[14]	魏晓辉, 许国威, 王兴旺, 徐海啸. 基于节点相似性和链接次数组合时间序列的链接预测[J]. 吉林大学学报(理学版), 2019, 57(3): 583-590.
[15]	刘久彪. 空间数据库反向最近邻聚类方法[J]. 吉林大学学报(理学版), 2019, 57(2): 387-392.