×

zbMATH — the first resource for mathematics

Improving the time efficiency of proving theorems using a learning mechanism. (English) Zbl 0976.68134
Summary: We develop a new approach for enhancing the time efficiency of proving theorems by using a learning mechanism. A system is proposed for analyzing a set of theorems and observing those features that often affect the speed at which the theorems are proved. The system uses the learning mechanism for choosing between two well known theorem-provers, namely, Resolution-Refutation (TGTP) and Semantic Trees (HERBY). A three-step process has been implemented. The first step is to prove a set of theorems using the above two theorem provers. A training set of two classes of theorems is thus created. Each class represents those theorems that have been proven in less time using a particular theorem prover. The second step is to train neural networks on both classes of theorems in order to construct an internal representation of the decision boundary between the two classes. In the last step, a voting scheme is invoked in order to combine the decisions of the individual neural networks into a final decision. The results achieved by the system when working on the standard theorems of the stickel test set are shown. Those results confirm the feasibility of our approach to integrate a learning mechanism into the process of automated theorem proving.
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
NeuroShell 2; TGTP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Almonayyes A., Ph.D. Thesis (1995)
[2] Almulla M., Ph.D. Thesis (1995)
[3] DOI: 10.1080/00207169608804524 · Zbl 1001.68513 · doi:10.1080/00207169608804524
[4] DOI: 10.1016/0893-6080(94)90046-9 · Zbl 00727861 · doi:10.1016/0893-6080(94)90046-9
[5] DOI: 10.1162/neco.1989.1.1.151 · doi:10.1162/neco.1989.1.1.151
[6] Bledsoe W., Machine Intelligence 9 pp 53– (1979)
[7] Chin-Lang C., Symbolic Logic and Mechanical Theorem Proving (1973) · Zbl 0263.68046
[8] Frederick M., Online Help manual of NeuroShell 2’s Software Package (1993)
[9] DOI: 10.1109/79.180705 · doi:10.1109/79.180705
[10] Kolodner J., Case-Based Reasoning (1993) · Zbl 0811.68055 · doi:10.1016/B978-1-55860-237-3.50005-4
[11] Lopes, R. and Tarver, M. 1997. Inducing Theorem Provers from Proofs. Proceedings of the Ninth IEEE International Conference on Published Tools with Artificial Intelligence. 1997. pp.157–164.
[12] Newborn M. The Great Theorem Prover, Version 2, Newborn Software 1992
[13] Normi H., Comparing Voting Systems (1994)
[14] DOI: 10.1145/321250.321253 · Zbl 0139.12303 · doi:10.1145/321250.321253
[15] Specht, D. and Romsdahl, H. 1994. Experience with Adaptive Probabilistic Neural Networks and Adaptive General Regression Neural Networks. IEEE World Congress on Computational Intelligence, Proceedings of International Conference on Artificial Neural Networks. 1994. Vol. 2, pp.1203–1208.
[16] Specht, D. and Shapiro, P. 1991. Generalization Accuracy Probabilistic Neural Net-works Compared with Back Propagation Networks. Proceedings of Seattle International Conference on Neural Networks. 1991. pp.887–892.
[17] DOI: 10.1007/BF00297245 · Zbl 0662.68104 · doi:10.1007/BF00297245
[18] Yu, Q., Almulla, M. and Newborn, M. 1996. Heuristics for a Semantics Tree Theorem Prover. Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics AIU MATH-96. 1996. pp.162–165. Florida Fort Lauderdale
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.