Paper Info
Title
Improving The Time Efficiency Of Proving Theorems Using A Learning Mechanism
Abstract
In this paper, 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.
Year
DOI
Venue
2001
10.1080/00207160108805059
INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS
Keywords
Field
DocType
semantic trees, resolution-refutation, learning mechanism, neural networks, automated theorem proving
HOL,Space hierarchy theorem,Voting,Algebra,Mathematical analysis,Automated theorem proving,First-order logic,Artificial neural network,Decision boundary,Semantics,Mathematics
Journal
Volume
Issue
ISSN
77
2
0020-7160
Citations 
PageRank 
References 
0
0.34
7
Authors
4
Name
Order
Citations
PageRank
Ahmed Almonayyes100.68
Hazem Raafat27116.23
Mohammed Almulla314720.60
Rana'a Alharshani400.34