Fuchs, M2015-12-130747-7171http://hdl.handle.net/1885/89815Automated 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 prover to find proofs significantly faster and to prove hard problems that were out of reach before.200010.1006/jsco.1999.03492015-12-12