矛盾体分离超演绎方法及应用

doi:10.11772/j.issn.1001-9081.2023101404

《计算机应用》唯一官方网站 ›› 2024, Vol. 44 ›› Issue (10): 3074-3080.DOI: 10.11772/j.issn.1001-9081.2023101404

矛盾体分离超演绎方法及应用

曹锋(), 杨小玲, 易见兵, 李俊

江西理工大学信息工程学院，江西赣州 341000

收稿日期:2023-10-19 修回日期:2024-02-08 接受日期:2024-02-21 发布日期:2024-10-15 出版日期:2024-10-10
通讯作者: 曹锋
作者简介:曹锋（1984—），男，江西上饶人，讲师，博士，主要研究方向：智能信息处理、自动推理、一阶逻辑自动定理证明器 caofeng19840301@163.com
杨小玲（2000—），女，江西抚州人，硕士研究生，主要研究方向：智能信息处理、自动推理、一阶逻辑自动定理证明器
易见兵（1980—），男，江西宜春人，副教授，博士，主要研究方向：人工智能
李俊（1984—），男，湖南益阳人，讲师，博士，主要研究方向：人工智能。
基金资助:
国家自然科学基金资助项目(62366017);江西省教育厅科研项目(GJJ200818);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金资助项目(205200100060)

Contradiction separation super-deduction method and application

Feng CAO(), Xiaoling YANG, Jianbing YI, Jun LI

School of Information Engineering，Jiangxi University of Science and Technology，Ganzhou Jiangxi 341000，China

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.
YI Jianbing， born in 1980， Ph. D.， associate professor. His research interests include artificial intelligence.
LI Jun， born in 1984， Ph. D.， lecturer. His research interests include artificial intelligence.
Supported by:
National Natural Science Foundation of China(62366017);General Research Project of Jiangxi Education Department(GJJ200818);Ganzhou Science and Technology Plan Project(GZKJ20206030);Doctorial Initiation Fund of Jiangxi University of Science and Technology(205200100060)

摘要/Abstract

摘要：

作为当前自动定理证明器中常用的推理机制，传统基于二元演绎超归结方法的推理过程限定每次有且只有2个子句参与演绎，这种分离的演绎步骤导致演绎缺失导向性和预判性，演绎效率有待提升。为了提升演绎效率，在理论上，针对传统的超归结方法引入多元演绎思想，提出矛盾体分离超演绎定义和方法，它具有多元性、动态性和导向性的演绎特性；在算法实现中，考虑子句参与演绎具有多元和协同特性，并灵活设定演绎的条件，提出一种具有回溯机制的矛盾体分离超演绎算法。将所提算法应用于Eprover3.1证明器，以国际自动定理证明器2023年竞赛例和TPTP（Thousands of Problems for Theorem Provers）问题库中难度系数为1的问题作为测试对象，在300 s内，应用所提算法的Eprover3.1证明器比原始Eprover3.1多证明了15个定理；当测试相同数量的定理时，所提算法的平均证明时间缩减了1.326 s，能够证明7个难度系数为1的定理。测试结果表明，所提算法能有效地应用于一阶逻辑自动定理证明，提升自动定理证明器的证明能力和效率。

关键词: 定理证明器, 二元演绎, 超归结, 多元演绎, 矛盾体分离

Abstract:

As a common inference mechanism in the current automated theorem prover， the traditional hyper-resolution method based on binary deduction is limited to only two clauses involved in each deduction step. The separated deduction steps lead to the lack of guidance and prediction of the binary chain deduction， and its deduction efficiency needs to be improved. To improve the efficiency of deduction， in theory， the idea of multi-clause deduction was introduced into the traditional method of super-resolution， the definition and method of the contradiction separation super-deduction were proposed，which had the deduction characteristics of multi-clause， dynamics and guidance. In the implementation of the algorithm， considering that the clause participation in deduction had multi-clause and synergized characteristics， and flexibly setting the deduction conditions， a contradiction separation super-deduction algorithm with backtracking mechanism was proposed. The proposed algorithm was applied to Eprover3.1 prover， taking the International Automated Theorem Prover Competition 2023 and the most difficult problems with a difficulty rating of 1 in the TPTP （Thousands of Problems for Theorem Provers） benchmark database as the test objects. Within 300 s， the Eprover3.1 prover with the proposed algorithm solved 15 theorems more than the original Eprover3.1 prover， and the average proof time was reduced by 1.326 s with the same total number of solved theorems， and 7 theorems with the rating of 1 could be solved. The test results show that the proposed algorithm can be effectively applied to automated theorem proving in first-order logic， improving the proof capability and efficiency of automated theorem prover.

Key words: theorem prover, binary deduction, super-resolution, multi-clause deduction, contradiction separation

中图分类号:

TP181

曹锋, 杨小玲, 易见兵, 李俊. 矛盾体分离超演绎方法及应用[J]. 计算机应用, 2024, 44(10): 3074-3080.

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.

图/表 9

图1 二元超归结演绎

Fig. 1 Binary super-resolution deduction

表1 矛盾体分离演绎过程

Tab. 1 Deductive process of contradiction separation

$C i$	$C i σ i +$	$C i σ i -$
$C 5$		$P 3 (a)$
$C 3$	$P 2 (c, b / x 3)$	$~ P 3 (a / x 2) ∨ P 4 (f (c), f (b))$
$C 4$	$P 1 (c, a)$	$~ P 2 (a, b) ∨ ~ P 4 (f (c) / x 4,$ $f (b) / x 5)$
$C 2$		$~ P 1 (c / x 1, a) ∨ P 2 (a / x 1, b) ∨$ $P 3 (b / x 3, f (b))$
$C 1$	$P 1 (f (a), a)$	$~ P 3 (b, f (b))$

表1 矛盾体分离演绎过程

Tab. 1 Deductive process of contradiction separation

$C i$	$C i σ i +$	$C i σ i -$
$C 5$		$P 3 (a)$
$C 3$	$P 2 (c, b / x 3)$	$~ P 3 (a / x 2) ∨ P 4 (f (c), f (b))$
$C 4$	$P 1 (c, a)$	$~ P 2 (a, b) ∨ ~ P 4 (f (c) / x 4,$ $f (b) / x 5)$
$C 2$		$~ P 1 (c / x 1, a) ∨ P 2 (a / x 1, b) ∨$ $P 3 (b / x 3, f (b))$
$C 1$	$P 1 (f (a), a)$	$~ P 3 (b, f (b))$

表2 第1次矛盾体分离超演绎过程

Tab. 2 First super-deduction process of contradiction separation

$C i$	$C i σ i + = C 6$	$C i σ i -$
$C 1$	$P 3 (b)$	$P 2 (f (b))$
$C 2$		$~ P 1 (a) ∨ ~ P 2 (f (b) / x 1)$
$C 4$	$P 2 (a)$	$P 1 (a / x 2)$

表2 第1次矛盾体分离超演绎过程

Tab. 2 First super-deduction process of contradiction separation

$C i$	$C i σ i + = C 6$	$C i σ i -$
$C 1$	$P 3 (b)$	$P 2 (f (b))$
$C 2$		$~ P 1 (a) ∨ ~ P 2 (f (b) / x 1)$
$C 4$	$P 2 (a)$	$P 1 (a / x 2)$

表3 第2次矛盾体分离超演绎过程

Tab. 3 Second super-deduction process of contradiction separation

$C i$	$C i σ i +$	$C i σ i -$
$C 3$		$~ P 4 (a / x 2) ∨ ~ P 3 (b / x 3) ∨ ~ P 2 (a)$
$C 5$		$P 4 (a)$
$C 6$		$P 2 (a) ∨ P 3 (b)$

表3 第2次矛盾体分离超演绎过程

Tab. 3 Second super-deduction process of contradiction separation

$C i$	$C i σ i +$	$C i σ i -$
$C 3$		$~ P 4 (a / x 2) ∨ ~ P 3 (b / x 3) ∨ ~ P 2 (a)$
$C 5$		$P 4 (a)$
$C 6$		$P 2 (a) ∨ P 3 (b)$

图2 本文算法流程

Fig. 2 Flow of proposed algorithm

图3 CSSD_E和Eprover3.1测试2023年竞赛例的性能对比

Fig. 3 Performance comparison between CSSD_E and Eprover3.1 for 2023 competition examples

表4 CSSD_E证明的17个定理判定情况

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

表5 CSSD_E证明的7个难度系数为1的定理

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

图4 CSSD_E和CSCD_E测试2023年竞赛例的性能对比

Fig. 4 Performance comparison between CSSD_E and CSCD_E for 2023 competition examples

参考文献 33

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]	陶文萱, 陈钢. 基于二幂阶矩阵的量子中间表示与翻译[J]. 《计算机应用》唯一官方网站, 2024, 44(10): 3141-3150.
[2]	郑焕张景中. 可由用户持续发展的几何自动推理平台的推理算法[J]. 计算机应用, 2011, 31(08): 2101-2104.

矛盾体分离超演绎方法及应用

Contradiction separation super-deduction method and application

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 9

参考文献 33

相关文章 2

编辑推荐

Metrics