Automated theorem proving essentially amounts to solving search problems. Despite significant progress in recent years theorem provers still have many shortcomings. The use of machine-learning techniques such as schemas is acknowledged as promising, but difficult to apply in the area of theorem proving. We propose a simple form of schemas, and to make use of a schema heuristically by integrating it with a search-guiding heuristic. Experiments have demonstrated that the approach allows a theorem...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.