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 scehma heuristically by integrating it with a search-guiding heuris- tic.
展开▼
