A new type of generic, self-evolving and efficient automated deduction algorithm based on category theory

Zijian Wang; Xinhui Shao; Zijian Wang; Xinhui Shao

doi:10.3934/math.2023929

AIMS Mathematics

2023, Volume 8, Issue 8: 18278-18294. doi: 10.3934/math.2023929

Previous Article Next Article

Research article

A new type of generic, self-evolving and efficient automated deduction algorithm based on category theory

Zijian Wang ¹,
Xinhui Shao ^{2
,
,}

1.
Northeast Yucai School, No.2, Gaogong Road, Shenyang, Liaoning, China
2.
Department of Mathematics, College of Sciences, Northeastern University, Shenyang, Liaoning, China

Received: 08 January 2023 Revised: 29 April 2023 Accepted: 19 May 2023 Published: 29 May 2023
MSC : 03B35, 68V15, 18-00, 18-04, 68W99

In this article, a new type of generalized, self-evolving and efficient automated statement proof algorithm based on new data structures, i.e., brackets and map graphs, and new algorithms is presented. The brackets structure provides an elegant low-knowledge representation of mathematical concepts. The map graphs offer an efficient machine-learning method which let the computer learn knowledge while proving. Additionally, the new finding is built completely on category theory. Furthermore, a prototype of the program is presented and examined for performance.
- automatic prover,
- theorem prover,
- algorithm,
- category theory,
- automatic deduction,
- automatic reasoning
Citation: Zijian Wang, Xinhui Shao. A new type of generic, self-evolving and efficient automated deduction algorithm based on category theory[J]. AIMS Mathematics, 2023, 8(8): 18278-18294. doi: 10.3934/math.2023929

Related Papers:

Abstract

In this article, a new type of generalized, self-evolving and efficient automated statement proof algorithm based on new data structures, i.e., brackets and map graphs, and new algorithms is presented. The brackets structure provides an elegant low-knowledge representation of mathematical concepts. The map graphs offer an efficient machine-learning method which let the computer learn knowledge while proving. Additionally, the new finding is built completely on category theory. Furthermore, a prototype of the program is presented and examined for performance.

References

[1]	S. Wolfram, Wolfram language & system documentation center, Wolfram Research Inc., Champaign, IL, US, 12Eds., 2019.
[2]	X. S. Gao, Geoexpert, Beijing, 1998. Available from: http://www.mmrc.iss.ac.cn/gex/.
[3]	L. D. Moura, S. Ullrich, The lean 4 theorem prover and programming language, Autom. Deduction -CADE, 2021,625–235. http://doi.org/10.1007/978-3-030-79876-5_37 doi: 10.1007/978-3-030-79876-5_37
[4]	L. D. Moura, N. Bjørner, Z3: An efficient smt solver, In: Tools and Algorithms for the Construction and Analysis of Systems, 4963 (2008), 337–340. http://doi.org/10.1007/978-3-540-78800-3_24
[5]	W. W. Li, Daishuxue Fangfa, 1 Ed, High Education Press, Beijing, 2019. ISBN 978-7-04-050725-6.
[6]	H. Ebbinghaus, Memory: A contribution to experimental psychology, Teachers College, Columbia University, New York City, 1913. Available from: https://archive.org/details/memorycontributi00ebbiuoft/page/n5/mode/2up.
[7]	K. Entacher, A collection of selected pseudorandom number generators with linear structures, 1997. Available from: https://www.semanticscholar.org/paper/6ae5fe88d296e70f188b0d12207d468c8f36e262.
[8]	A. S. Tanenbaum, Operating systems: Design and implementation (volume 1), Publishing House of Electronics Industry, Beijing, 3 Eds., 2015. ISBN 978-7-121-26193-0.
[9]	Z. J. Wang, The defqed repository, 2022. Available from: https://github.com/ZijianFelixWang/DefQed.
[10]	Z. J. Wang, Benchmark of the defqed algorithm, 2022. Available from: https://github.com/ZijianFelixWang/DefQed-Benchmark.
[11]	H. Packard, The hp zbook 14u g5 specifications, 2018. https://support.hp.com/us-en/document/c05873311.

Reader Comments

Your name:*

Email:*
© 2023 the Author(s), licensee AIMS Press. This is an open access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0)