Clause reusing framework for contradiction separation based automated deduction

被引:0
|
作者
Chen, Shuwei [1 ]
Xu, Yang [1 ]
Liu, Jun [2 ]
Cao, Feng [3 ]
Jiang, Yan [3 ]
机构
[1] Southwest Jiaotong Univ, Sch Math, Chengdu 610031, Peoples R China
[2] Ulster Univ, Sch Comp, Coleraine, Londonderry, North Ireland
[3] Southwest Jiaotong Univ, Sch Informat Sci & Technol, Chengdu 610031, Peoples R China
基金
中国国家自然科学基金;
关键词
Logic; Automated reasoning; Contradiction separation deduction; Clause; Literal;
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Guidance ability is one of the typical feature of the novel contradiction separation based automated deduction that extends the canonical resolution rule to a dynamic, flexible multi-clause deduction framework. In order to take better advantage of the guidance ability during the deduction process, we propose in this paper a clause reusing framework for contradiction separation based automated deduction. This framework is able to generate more decision literals, on which the guidance ability of the contradiction separation based automated deduction relies. Technical analysis along with some examples are provided to illustrate the feasibility of the proposed framework.
引用
收藏
页码:284 / 291
页数:8
相关论文
共 50 条
  • [1] Fully reusing clause deduction algorithm based on standard contradiction separation rule
    Liu, Peiyao
    Xu, Yang
    Liu, Jun
    Chen, Shuwei
    Cao, Feng
    Wu, Guanfeng
    INFORMATION SCIENCES, 2023, 622 : 337 - 356
  • [2] Preliminary framework to combine contradiction separation based automated deduction with superposition and given-clause algorithm
    Ning, Xinran
    Xu, Yang
    Cao, Feng
    Liu, Jun
    DATA SCIENCE AND KNOWLEDGE ENGINEERING FOR SENSING DECISION SUPPORT, 2018, 11 : 774 - 781
  • [3] Contradiction separation based dynamic multi-clause synergized automated deduction
    Xu, Yang
    Liu, Jun
    Chen, Shuwei
    Zhong, Xiaomei
    He, Xingxing
    INFORMATION SCIENCES, 2018, 462 : 93 - 113
  • [4] Some Synergized Clause Selection Strategies for Contradiction Separation Based Automated Deduction
    Chen, Shuwei
    Xu, Yang
    Jiang, Yan
    Liu, Jun
    He, Xingxing
    2017 12TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (IEEE ISKE), 2017,
  • [5] Look-ahead clause selection strategy for contradiction separation based automated deduction
    Chen, Shuwei
    Xu, Yang
    Liu, Jun
    Cao, Feng
    DATA SCIENCE AND KNOWLEDGE ENGINEERING FOR SENSING DECISION SUPPORT, 2018, 11 : 750 - 757
  • [6] A complementary ratio based clause selection method for contradiction separation dynamic deduction
    Zeng, Guoyan
    Chen, Shuwei
    Liu, Jun
    Xu, Yang
    Liu, Peiyao
    KNOWLEDGE-BASED SYSTEMS, 2024, 284
  • [7] Distinctive features of the contradiction separation based dynamic automated deduction
    Xu, Yang
    Chen, Shuwei
    Liu, Jun
    Zhong, Xiaomei
    He, Xingxing
    DATA SCIENCE AND KNOWLEDGE ENGINEERING FOR SENSING DECISION SUPPORT, 2018, 11 : 725 - 732
  • [8] A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
    Cao, Feng
    Xu, Yang
    Liu, Jun
    Chen, Shuwei
    Yi, Jianbing
    INFORMATION SCIENCES, 2021, 566 : 281 - 299
  • [9] An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capability
    Liu, Peiyao
    Chen, Shuwei
    Liu, Jun
    Xu, Yang
    Cao, Feng
    Wu, Guanfeng
    KNOWLEDGE-BASED SYSTEMS, 2023, 261
  • [10] A new strategy for preventing repeated and redundant clauses in contradiction separation based automated deduction
    He, Xingxing
    Xu, Y.
    Liu, J.
    Qiu, Xiaoping
    Li, Yingfang
    DATA SCIENCE AND KNOWLEDGE ENGINEERING FOR SENSING DECISION SUPPORT, 2018, 11 : 790 - 797