[1] |
Kovács L.Symbolic computation and automated reasoning for program analysis[C]∥Proc of the 12th International Conference on Integrated Formal Methods,2016:20-27.
|
[2] |
Cao Feng, Xu Yang,Chen Shu-wei,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-408.(in Chinese)
|
[3] |
Kovács L, Voronkov A.First-order theorem proving and Vampire[C]∥Proc of the 25th International Conference on Computer Aided Verification,2013:1-35.
|
[4] |
Schulz S,Cruanes S,Vukmirovi P.Faster,higher,stronger:E 2.3[C]∥Proc of the 27th International Conference on Automated Deduction,2019:495-507.
|
[5] |
Korovin K. iProver—An instantiation-based theorem prover for first-order logic[C]∥Proc of the 4th International Joint Conference on Automated Reasoning,2009:292-298.
|
[6] |
McCune W. Release of Prover9[C]∥Proc of the Mile High Conference on Quasigroups,Loops and Nonassociative Systems,2005:1.
|
[7] |
Schulz S,Mhrmann M.Performance of clause selection heuristics for saturation-based theorem proving[C]∥Proc of the 8th International Joint Conference on Automated Reasoning,2016:330-345.
|
[8] |
Reger G,Tishkovsky D,Voronkov A.CoopeRating proof attempts[C]∥Proc of the 25th International Conference on Automated Deduction,2015:339-355.
|
[9] |
Jakubuv J,Urban J.Extending E prover with similarity based clause selection strategies[C]∥Proc of the 9th International Conference on Intelligent Computer Mathematics,2016:151-156.
|
[10] |
Cao F,Xu Y,Zhong J,et al.Holistic deductive framework theorem proving based on standard contradiction separation for first-order logic[C]∥Proc of the 12th International Conference on Intelligent Systems and Knowledge Engineering,2017:389-393.
|
[11] |
Rawson M, Reger G.Old or heavy? Decaying gracefully with age/weight shapes[C]∥Proc of the 27th International Conference on Automated Deduction,2019:462-476.
|
[12] |
Jakubuv J,Kaliszyk C.Relaxed weighted path order in theorem proving[J].Mathematics in Computer Science,2020,14(1):657-670.
|
[13] |
Cao F, Xu Y,Liu J,et al. A multi-clause dynamic deduction algorithm based on standard contradiction separation rule[J].Information Sciences,2021,566:281-299.
|
[14] |
Xu Y,Liu J,Chen S W, et al.Contradiction separation based dynamic multi-clause synergized automated deduction[J].Information Sciences,2018,462(1):93-113.
|
[15] |
Cao Feng, Xu Yang,Wu Guan-feng,et al.Application of multi-clause dynamic deduction in Prover9[J].Computer Engineering & Science,2019,41(9):1686-1692.(in Chinese)
|
[16] |
Robinson J A.A machine-oriented logic based on the resolution principle[J].Journal of the ACM,1965,12(1):23-41.
|
[17] |
Robinson J A.Automatic deduction with hyper-resolution[J].International Journal of Computing & Mathematics,1965,1(3):227-234.
|
[18] |
Overbeek R,Mccharen J,Wos L.Complexity and related enhancements for automated theorem-proving programs[J].Computers & Mathematics with Applications,1976,2(1):1-16.
|
[19] |
Loveland D W.A linear format for resolution[C]∥Proc of the International IRIA Symposium on Automatic Demonstration,1970:147-162.
|
[20] |
Cao F, Xu Y, Liu J, et al.CSE_E 1.0:An integrated automated theorem prover for first-order logic[J].Symmetry,2019,11(9):1142.1-1142.15.
|
[21] |
Cao F,Xu Y,Chen S W,et al.A contradiction separation dynamic deduction algorithm based on optimized proof search[J].The International Journal of Computational Intelligence Systems,2019,12(2):1245-1254.
|
|
附中文参考文献:
|
[2] |
曹锋,徐扬,陈树伟,等.多元协同演绎在一阶逻辑ATP中的应用[J].西南交通大学学报,2020,55(2):401-408.
|
[15] |
曹锋,徐扬,吴贯锋,等.多元动态演绎在Prover9证明器中的应用[J].计算机工程与科学,2019,41(9):1686-1692.
|