Distinctive features of the contradiction separation based dynamic automated deduction

被引：0

作者：

Xu, Yang ^{[1
,3
]}

Chen, Shuwei ^{[1
,3
]}

Liu, Jun ^{[2
,3
]}

Zhong, Xiaomei ^{[1
,3
]}

He, Xingxing ^{[1
,3
]}

机构：

[1] Southwest Jiaotong Univ, Sch Math, Chengdu 610031, Sichuan, Peoples R China

[2] Ulster Univ, Sch Comp & Math, Coleraine, Londonderry, North Ireland

[3] Southwest Jiaotong Univ, Natl Local Joint Engn Lab Syst Credibil Automat V, Chengdu 610031, Sichuan, Peoples R China

来源：

DATA SCIENCE AND KNOWLEDGE ENGINEERING FOR SENSING DECISION SUPPORT | 2018年 / 11卷

基金：

中国国家自然科学基金;

关键词：

Resolution; automated deduction; contradiction; contradiction separation;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Contradiction separation based dynamic automated deduction is a novel development of the standard static (i.e., fixed) binary resolution into a dynamic multi-clause synergized contradiction separation based inference rule. In this paper, we consider some distinctive features/advantages of this novel automated deduction mechanism, including multi-clause involvement, dynamic deduction, synergized deduction, robustness, exchangeability, controllability, scaling, repeatability, integrity and flexibility, along with some illustrative examples.

引用

页码：725 / 732

页数：8

共 9 条

[1] Bonacina M. P., 2017, 1 INT ARCADE WORKSH
[2] Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses
Gorzny, Jan
Paleo, Bruno Woltzenlogel
[J]. AUTOMATED DEDUCTION - CADE-25, 2015, 9195 : 356 - 366
[3] Kovacs L., 2013, 1 ORDER THEOREM PROV
[4] History and Prospects for First-Order Automated Deduction
Plaisted, David A.
[J]. AUTOMATED DEDUCTION - CADE-25, 2015, 9195 : 3 - 28
[5] A MACHINE-ORIENTED LOGIC BASED ON RESOLUTION PRINCIPLE
ROBINSON, JA
[J]. JOURNAL OF THE ACM, 1965, 12 (01) : 23 - &
[6] Schulz S., 2013, LECT NOTES COMPUTER, V51, P1927
[7] Weidenbach C, 2009, LECT NOTES ARTIF INT, V5663, P140, DOI 10.1007/978-3-642-02959-2_10
[8] Xu Y., 2018, CONTRADICTION SEPARA
[9] Xu Y, 2016, WD SCI P COMP ENG, V10, P483

← 1 →