Journal of Computer Applications ›› 2024, Vol. 44 ›› Issue (10): 3074-3080.DOI: 10.11772/j.issn.1001-9081.2023101404
• Artificial intelligence • Previous Articles Next Articles
Feng CAO(), Xiaoling YANG, Jianbing YI, Jun LI
Received:
2023-10-19
Revised:
2024-02-08
Accepted:
2024-02-21
Online:
2024-10-15
Published:
2024-10-10
Contact:
Feng CAO
About author:
YANG Xiaoling, born in 2000, M. S. candidate. Her research interests include intelligent information processing, automated reasoning, first-order logic automated theorem prover.Supported by:
通讯作者:
曹锋
作者简介:
曹锋(1984—),男,江西上饶人,讲师,博士,主要研究方向:智能信息处理、自动推理、一阶逻辑自动定理证明器 caofeng19840301@163.com基金资助:
CLC Number:
Feng CAO, Xiaoling YANG, Jianbing YI, Jun LI. Contradiction separation super-deduction method and application[J]. Journal of Computer Applications, 2024, 44(10): 3074-3080.
曹锋, 杨小玲, 易见兵, 李俊. 矛盾体分离超演绎方法及应用[J]. 《计算机应用》唯一官方网站, 2024, 44(10): 3074-3080.
Add to citation manager EndNote|Ris|BibTeX
URL: https://www.joca.cn/EN/10.11772/j.issn.1001-9081.2023101404
定理名称 | 难度系数 | 证明时间/s | 子句数 | 文字数 |
---|---|---|---|---|
平均值 | 0.78 | 233.557 | 2 152 | 24 086 |
CSR249+1 | 0.97 | 219.796 | 7 433 | 16 528 |
GEO345+1 | 0.97 | 250.154 | 130 | 1 378 |
SEU237+1 | 0.94 | 233.080 | 67 | 170 |
CSR240+1 | 0.92 | 207.755 | 7 433 | 16 529 |
BIO005+1 | 0.92 | 125.057 | 9 161 | 347 191 |
SWW099+1 | 0.86 | 232.008 | 45 | 99 |
CSR237+1 | 0.83 | 206.028 | 7 433 | 16 529 |
SWB066+1 | 0.83 | 252.516 | 560 | 1 791 |
AGT008+1 | 0.81 | 266.471 | 556 | 656 |
SWC341+1 | 0.81 | 271.103 | 96 | 408 |
AGT011+1 | 0.78 | 259.265 | 556 | 656 |
AGT022+1 | 0.69 | 180.838 | 556 | 656 |
SWB014+1 | 0.61 | 280.042 | 560 | 1 782 |
HAL001+2 | 0.58 | 141.110 | 33 | 94 |
SWB025+1 | 0.58 | 280.048 | 560 | 1 789 |
ALG072+1 | 0.58 | 283.310 | 9 | 44 |
SWW470+3 | 0.56 | 281.883 | 1 399 | 3 162 |
Tab. 4 Details of 17 theorems solved by CSSD_E
定理名称 | 难度系数 | 证明时间/s | 子句数 | 文字数 |
---|---|---|---|---|
平均值 | 0.78 | 233.557 | 2 152 | 24 086 |
CSR249+1 | 0.97 | 219.796 | 7 433 | 16 528 |
GEO345+1 | 0.97 | 250.154 | 130 | 1 378 |
SEU237+1 | 0.94 | 233.080 | 67 | 170 |
CSR240+1 | 0.92 | 207.755 | 7 433 | 16 529 |
BIO005+1 | 0.92 | 125.057 | 9 161 | 347 191 |
SWW099+1 | 0.86 | 232.008 | 45 | 99 |
CSR237+1 | 0.83 | 206.028 | 7 433 | 16 529 |
SWB066+1 | 0.83 | 252.516 | 560 | 1 791 |
AGT008+1 | 0.81 | 266.471 | 556 | 656 |
SWC341+1 | 0.81 | 271.103 | 96 | 408 |
AGT011+1 | 0.78 | 259.265 | 556 | 656 |
AGT022+1 | 0.69 | 180.838 | 556 | 656 |
SWB014+1 | 0.61 | 280.042 | 560 | 1 782 |
HAL001+2 | 0.58 | 141.110 | 33 | 94 |
SWB025+1 | 0.58 | 280.048 | 560 | 1 789 |
ALG072+1 | 0.58 | 283.310 | 9 | 44 |
SWW470+3 | 0.56 | 281.883 | 1 399 | 3 162 |
定理名称 | 子句数 | 最大项深度 | 变元项数 | 证明时间/s |
---|---|---|---|---|
平均值 | 3 202 | 6 | 8 221 | 249.885 |
SEU410+3 | 19 045 | 7 | 50 536 | 130.275 |
SET345-6 | 114 | 6 | 214 | 247.987 |
NUM090-1 | 161 | 6 | 303 | 298.123 |
NUM428+1 | 23 | 3 | 37 | 265.640 |
SWV276-1 | 2 898 | 8 | 6 080 | 291.955 |
LAT077-1 | 2 | 9 | 4 | 250.043 |
ALG001-1 | 171 | 4 | 388 | 265.174 |
Tab. 5 Seven theorems with difficulty rating of 1 solved by CSSD_E
定理名称 | 子句数 | 最大项深度 | 变元项数 | 证明时间/s |
---|---|---|---|---|
平均值 | 3 202 | 6 | 8 221 | 249.885 |
SEU410+3 | 19 045 | 7 | 50 536 | 130.275 |
SET345-6 | 114 | 6 | 214 | 247.987 |
NUM090-1 | 161 | 6 | 303 | 298.123 |
NUM428+1 | 23 | 3 | 37 | 265.640 |
SWV276-1 | 2 898 | 8 | 6 080 | 291.955 |
LAT077-1 | 2 | 9 | 4 | 250.043 |
ALG001-1 | 171 | 4 | 388 | 265.174 |
1 | VUKMIROVIĆ P, BENTKAMP A, BLANCHETTE J, et al. Making higher-order superposition work[J]. Journal of Automated Reasoning, 2022, 66: 541-564. |
2 | BENTKAMP A, BLANCHETTE J, TOURRET S, et al. Superposition for full higher-order logic[C]// Proceedings of the 28th International Conference on Automated Deduction. Cham: Springer, 2021: 396-412. |
3 | 邹宇,彭翕成,饶永生.基于吴方法的几何定理证明的恒等式方法[J].中国科学: 数学,2021,51(1):289-300. |
ZOU Y, PENG X C, RAO Y S. An identity method for proving geometry theorems based on Wu’s method[J]. SCIENTIA SINICA Mathematica,2021,51(1):289-300. | |
4 | CAILLER J, ROSAIN J, DELAHAYE D, et al. Goéland: a concurrent tableau-based theorem prover (system description) [C]// Proceedings of the 11th International Joint Conference on Automated Reasoning. Cham: Springer, 2022: 359-368. |
5 | 曹锋, 徐扬, 陈树伟, 等. 多元协同演绎在一阶逻辑ATP中的应用[J]. 西南交通大学学报, 2020, 55(2):401-409. |
CAO F, XU Y, CHEN S W, et.al. Application of multi-clause synergized deduction in first-order logic automated theorem proving[J]. Journal of Southwest Jiaotong University, 2020, 55(2):401-409. | |
6 | 刘清华.面向大理论的一阶逻辑前提选择研究[D].成都:西南交通大学,2021:1-4. |
LIU Q H. Study on first-order logical premise selection over large theories[D]. Chengdu: Southwest Jiaotong University, 2021:1-4. | |
7 | TAMMET T, SUTCLIFFE G. Combining JSON-LD with first order logic[C]// Proceedings of the 2021 IEEE 15th International Conference on Semantic Computing. Piscataway: IEEE, 2021: 256-261. |
8 | SINNER A, KLEEMANN T. KRHyper: in your pocket[C]// Proceedings of the 20th International Conference on Automated Deduction. Cham: Springer, 2005: 452-457. |
9 | TAMMET T, DRAHEIM D, JÄRV P. Confidences for commonsense reasoning[C]// Proceedings of the 28th International Conference on Automated Deduction. Cham: Springer, 2021: 507-524. |
10 | SABRI K E. Automated verification of role-based access control policies constraints using Prover9[EB/OL]. [2023-10-15]. . |
11 | TAMMET T, DRAHEIM D, JÄRV P. GK: implementing full first order default logic for commonsense reasoning (system description) [C]// Proceedings of the 11th International Joint Conference on Automated Reasoning. Cham: Springer, 2022: 300-309. |
12 | SIMIĆ D, MARIĆ F, BOUTRY P. Formalization of the Poincaré disc model of hyperbolic geometry[J]. Journal of Automated Reasoning, 2021, 65: 31-73. |
13 | ROBINSON J A. Automatic deduction with hyper-resolution[J]. International Journal of Computer Mathematics, 1965, 1(3): 227-234. |
14 | REGER G, TISHKOVSKY D, VORONKOV A. Cooperating proof attempts[C]// Proceedings of the 25th International Conference on Automated Deduction. Cham: Springer, 2015: 339-355. |
15 | HODER K, REGER G, SUDA M, et al. Selecting the selection[C]// Proceedings of the 8th International Joint Conference on Automated Reasoning. Cham: Springer, 2016: 313-329. |
16 | KISEL B, SUDA M. A unifying principle for clause elimination in first-order logic[C]// Proceedings of the 26th International Conference on Automated Deduction. Cham: Springer, 2017: 274-290. |
17 | 曾国艳,徐扬,陈树伟,等.基于多属性决策的一阶逻辑子句选择方法[J/OL].西南交通大学学报,2023:1-8[2023-10-01]. . |
ZENG G Y, XU Y, CHEN S W, et al. First-order logic clause selection method based on multi-criteria decision making[J/OL]. Journal of Southwest Jiaotong University, 2023:1-8[2023-10-01]. . | |
18 | XU Y, LIU J, CHEN S, et al. Contradiction separation based dynamic multi-clause synergized automated deduction[J]. Information Sciences, 2018, 462:93-113. |
19 | CHEN S, XU Y, LIU J, et al. Clause reusing framework for contradiction separation based automated deduction[C]// Developments of Artificial Intelligence Technologies in Computation and Robotics. [S.l.]: World Scientific, 2020: 284-291. |
20 | VUKMIROVIĆ P, BLANCHETTE J, SCHULZ S. Extending a high-performance prover to higher-order logic[C]// Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer, 2023: 111-129. |
21 | XU Y, LIU J, CHEN S W, et al. A novel generalization of resolution principle for automated deduction[C]// Uncertainty Modelling in Knowledge Engineering and Decision Making. [S.l.]: World Scientific, 2016: 483-488. |
22 | 林玲瑜,曹锋,易见兵,等.基于子句活跃度和复杂度的多元动态演绎算法及应用[J].计算机工程与科学, 2023,45(12): 2256-2264. |
LIN L Y, CAO F, YI J B, et al. A multi-clause dynamic deduction algorithm based on clause activity and complexity and its application[J]. Computer Engineering & Science, 2023,45(12): 2256-2264. | |
23 | LIU P, XU Y, LIU J, et al. Fully reusing clause deduction algorithm based on standard contradiction separation rule[J]. Information Sciences, 2023, 622: 337-356. |
24 | 唐雷明. 命题逻辑中完全标准矛盾体结构的研究[D].成都:西南交通大学,2021:18-30. |
TANG L M. The study of standard contradiction based on propositional logic[D]. Chengdu: Southwest Jiaotong University, 2021:18-30. | |
25 | 姜世攀,陈树伟,曾国艳.一阶逻辑定理证明器中的无效子句删除策略[J].计算机应用, 2024, 44(3): 677-682. |
JIANG S P, CHEN S W, ZENG G Y. Strategy of invalid clause elimination in first-order logic theorem prover[J].Journal of Computer Applications, 2024, 44(3): 677-682. | |
26 | 曹锋,郭海林,易见兵,等.基于矛盾体分离的多元冲突演绎方法及应用[J/OL].武汉大学学报(理学版):1-9[2023-12-31] .. |
CAO F, GUO H L, YI J B, et al. A multi-clause conflict deduction method based on contradiction separation and its application[J/OL]. Journal of Wuhan University (Natural Science Edition):1-9[2023-12-31]. . | |
27 | SUTCLIFFE G. The TPTP problem library and associated infrastructure: from CNF to TH0, TPTP v64.0[J]. Journal of Automated Reasoning, 2017, 59:483-502. |
28 | AFFELDT R, GARRIGUE J, SAIKAWA T. A library for formalization of linear error-correcting codes[J]. Journal of Automated Reasoning, 2020, 64:1123-1164. |
29 | GONTHIER G. The four colour theorem: engineering of a formal proof[C]// Proceedings of the 8th Asian Symposium on Computer Mathematics. Cham: Springer, 2007: 333. |
30 | 曹锋.一种基于矛盾体分离演绎的一阶逻辑自动定理证明器研究[D]. 成都:西南交通大学,2020:16-30. |
CAO F. Study on a first-order logic automated theorem prover based on contradiction separation deduction[D]. Chengdu: Southwest Jiaotong University, 2020:16-30. | |
31 | SCHULZ S, CRUANES S, VUKMIROVIĆ P. Faster, higher, stronger: E 2.3[C]// Proceedings of the 27th International Conference on Automated Deduction. Cham: Springer, 2019: 495-507. |
32 | SCHULZ S. System description: E 1.8[C]// Proceedings of the 19th International Conference on Logic for Programming Artificial Intelligence and Reasoning. Cham: Springer, 2013: 735-743. |
33 | McCUNE W. Release of prover9[EB/OL]. (2005-06-28) [2023-10-01]. . |
[1] | Lin GUO, Kunhu LIU, Chenyang MA, Youxue LAI, Yingfen XU. Image super-resolution reconstruction based on residual attention network with receptive field expansion [J]. Journal of Computer Applications, 2024, 44(5): 1579-1587. |
[2] | Zihan LIU, Dengwen ZHOU, Yukai LIU. Image super-resolution network based on global dependency Transformer [J]. Journal of Computer Applications, 2024, 44(5): 1588-1596. |
[3] | Yang LIU, Rong LIU, Ke FANG, Xinyue ZHANG, Guangxu WANG. Video super-resolution reconstruction network based on frame straddling optical flow [J]. Journal of Computer Applications, 2024, 44(4): 1277-1284. |
[4] | Wenxuan TAO, Gang CHEN. Quantum intermediate representation and translation based on power-of-two matrix [J]. Journal of Computer Applications, 2024, 44(10): 3141-3150. |
[5] | Hao CHEN, Zhenping XIA, Cheng CHENG, Xing LIN-LI, Bowen ZHANG. Lightweight image super-resolution reconstruction network based on Transformer-CNN [J]. Journal of Computer Applications, 2024, 44(1): 292-299. |
[6] | Min LIANG, Jiayi LIU, Jie LI. Image super-resolution reconstruction method based on iterative feedback and attention mechanism [J]. Journal of Computer Applications, 2023, 43(7): 2280-2287. |
[7] | Lihua SHEN, Bo LI. Super-resolution reconstruction of lung CT images based on feature pyramid network and dense network [J]. Journal of Computer Applications, 2023, 43(5): 1612-1619. |
[8] | Ying LI, Chao HUANG, Chengdong SUN, Yong XU. Single image super-resolution method based on residual shrinkage network in real complex scenes [J]. Journal of Computer Applications, 2023, 43(12): 3903-3910. |
[9] | Yining WANG, Qingshan ZHAO, Pinle QIN, Yulan HU, Chunmei ZONG. Super-resolution reconstruction algorithm of medical image based on lightweight dense neural network [J]. Journal of Computer Applications, 2022, 42(8): 2586-2592. |
[10] | Yingying ZHANG, Chao REN, Ce ZHU. Depth image super-resolution based on shape-adaptive non-local regression and non-local gradient regularization [J]. Journal of Computer Applications, 2022, 42(6): 1941-1949. |
[11] | Jia LI, Yuanlin ZHENG, Kaiyang LIAO, Haojie LOU, Shiyu LI, Zehao CHEN. No-reference image quality assessment algorithm based on saliency deep features [J]. Journal of Computer Applications, 2022, 42(6): 1957-1964. |
[12] | Huifeng WANG, Yan XU, Yiming WEI, Huizhen WANG. Image super-resolution reconstruction based on parallel convolution and residual network [J]. Journal of Computer Applications, 2022, 42(5): 1570-1576. |
[13] | Ye ZHANG, Rong LIU, Ming LIU, Ming CHEN. Image super-resolution reconstruction network based on multi-channel attention mechanism [J]. Journal of Computer Applications, 2022, 42(5): 1563-1569. |
[14] | Pengwei LIU, Yuan GAO, Pinle QIN, Zhe YIN, Lifang WANG. Medical MRI image super-resolution reconstruction based on multi-receptive field generative adversarial network [J]. Journal of Computer Applications, 2022, 42(3): 938-945. |
[15] | Junbo LI, Pinle QIN, Jianchao ZENG, Meng LI. CT three-dimensional reconstruction algorithm based on super-resolution network [J]. Journal of Computer Applications, 2022, 42(2): 584-591. |
Viewed | ||||||
Full text |
|
|||||
Abstract |
|
|||||